Fix

cvc5 · Jan 31, 2024 · 3ea1dc9 · 3ea1dc9
1 parent 70d37fa
commit 3ea1dc9
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 4 deletions.
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -185,7 +185,8 @@ Expr ExprParser::parseExpr()
               // will parse a tuple term that stands for a symbolic bound
               // variable list. We do this because there are no terms that
               // begin ((... currently allowed in this parser.
-              if (d_lex.peekToken()==Token::LPAREN && d_lex.peekToken()==Token::LPAREN)
+              if (d_lex.peekToken()==Token::LPAREN &&
+                  d_lex.peekToken()==Token::LPAREN)
               {
                 nscopes = 1;
                 bool isLookup = !d_state.getOptions().d_binderFresh;

diff --git a/src/lexer.cpp b/src/lexer.cpp
@@ -111,11 +111,10 @@ Token Lexer::nextToken()
 {
   if (d_peeked.empty())
   {
-    // Call the derived yylex() and convert it to a token
     return nextTokenInternal();
   }
-  Token t = d_peeked.back();
-  d_peeked.pop_back();
+  Token t = d_peeked[0];
+  d_peeked.erase(d_peeked.begin());
   return t;
 }
 

diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3
@@ -25,3 +25,9 @@
   :conclusion false)
 
 (step @p3 false :rule q-rule :premises (@p2))
+
+
+(declare-const f_list (-> Int @List))
+(declare-const a Int)
+
+(assume @pf (forall (f_list a) false))