From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 4 Jul 2010 07:45:38 +0000 (+0000)
Subject: Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9827a85ee8fae10bd964a3dd7999673515ce38a7;p=francis%2Fstp.git

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




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 1941641..c4f6af5 100644
--- 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