From 811ab517db7a23a293e7519baf529e9ed8772fe9 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 Jan 2011 04:52:39 +0000
Subject: [PATCH] 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
---
 src/parser/smtlib.y    | 14 ++++++--------
 src/parser/smtlib2.lex |  1 -
 2 files changed, 6 insertions(+), 9 deletions(-)

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."); }
 %%
-- 
2.47.3