Better

cvc5 · Jan 24, 2024 · e58abe9 · e58abe9
1 parent c75e4dc
commit e58abe9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -671,6 +671,10 @@ std::vector<Expr> ExprParser::parseAndBindSortedVarList(bool isLookup)
       // lookup and type check
       v = getVar(name);
       typeCheck(v, t);
+      if (v.getKind()!=Kind::VARIABLE)
+      {
+        d_lex.parseError("Expected a variable in binder");
+      }
     }
     else
     {

diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3
@@ -2,8 +2,8 @@
 
 (declare-const P (-> Int Bool))
 (declare-const forall (-> Bool Bool) :binder)
-(declare-const x Int)
-(declare-const z Int)
+(declare-var x Int)
+(declare-var z Int)
 
 (declare-rule id ((y Bool)) :premises (y) :conclusion y)