diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp index 46db402b..9f9ee806 100644 --- 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 index d322ac9f..68fc9fc0 100644 --- a/src/state.cpp +++ b/src/state.cpp @@ -755,7 +755,9 @@ Expr State::mkExpr(Kind k, const std::vector& 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; } } }