The gulwani smtlib tests require arity > 2 bvplus and bvmult. It's not part of the...

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 d3ca6464f996ecd94cb7a36652099316b40e156e..53f7f705ae7a6532d46f16eea8bfbc98c24875d9 100644 (file)
--- 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 7b27f2057bf3060554f6c8114dd0178370ac16c9..5f82b7dbdfdc3bbabda73362a4a1557d6bd0af4f 100644 (file)
--- 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."); }
 %%