From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 Jan 2011 04:52:39 +0000 (+0000)
Subject: The gulwani smtlib tests require arity > 2 bvplus and bvmult. It's not part of the... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=811ab517db7a23a293e7519baf529e9ed8772fe9;p=francis%2Fstp.git

The gulwani smtlib tests require arity > 2 bvplus and bvmult. It's not part of the specification, but it's easy to include...

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

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index d3ca646..53f7f70 100644
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -852,22 +852,20 @@ BITCONST_TOK { $$ = $1; }
   delete $2;
   delete $3;
 }
-|  BVPLUS_TOK an_term an_term 
+|  BVPLUS_TOK an_terms 
 {
-  const unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2, *$3));
+  const unsigned int width = (*$2)[0].GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2));
   $$ = n;
   delete $2;
-  delete $3;
 
 }
-|  BVMULT_TOK an_term an_term 
+|  BVMULT_TOK an_terms 
 {
-  const unsigned int width = $2->GetValueWidth();
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMULT, width, *$2, *$3));
+  const unsigned int width = (*$2)[0].GetValueWidth();
+  ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMULT, width, *$2));
   $$ = n;
   delete $2;
-  delete $3;
 }
 
 |      BVDIV_TOK an_term an_term  
diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 7b27f20..5f82b7d 100644
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -254,5 +254,4 @@ bv{DIGIT}+	{ smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 \|([^\|]|\n)*\| {return lookup(smt2text);}
 
 . { smt2error("Illegal input character."); }
-"\n" { smt2error("Illegal input character."); }
 %%