Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@916 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 1941641c56b625acb15004518ff5475f485d7c52..c4f6af52b9e3a626412a23c46f821f8762f3b293 100644 (file)
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -61,7 +61,14 @@
    
   static int lookup(const char* s)
   {
-    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(s); 
+    string str(s);
+  
+    // The SMTLIB2 specifications sez that the outter bars aren't part of the
+    // name. This means that we can create an empty string symbol name.
+    if (s[0] == '|' && s[str.size()-1] == '|')
+       str = str.substr(1,str.length()-2);
+    
+    BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(str.c_str()); 
 
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting