Fix spurious warnings

cvc5 · Mar 30, 2024 · 77c6b57 · 77c6b57
1 parent c5c4d35
commit 77c6b57
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
@@ -525,7 +525,7 @@ Expr ExprParser::parseExpr()
               Trace("parser") << "Binder is " << vl << std::endl;
               Trace("parser") << "Env is " << env << std::endl;
               // make the program variable, whose type is abstract
-              Expr ftype = d_state.mkFunctionType(fargTypes, atype);
+              Expr ftype = d_state.mkFunctionType(fargTypes, atype, false);
               std::stringstream pvname;
               pvname << "_match_" << hd;
               Expr pv = d_state.mkSymbol(Kind::PROGRAM_CONST, pvname.str(), ftype);

diff --git a/src/state.cpp b/src/state.cpp
@@ -755,7 +755,9 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
         }
         else
         {
-          Warning() << "Wrong number of arguments when applying program " << Expr(hd) << std::endl;
+          Warning() << "Wrong number of arguments when applying program " << Expr(hd)
+                    << ", " << t.getNumChildren() << " arguments expected, got "
+                    << children.size() << std::endl;
         }
       }
     }