Fix arguments to print callback (#4171)

The method applyParseOp may modify the argument vector. In the case of the sygus V1 parser, this argument vector was then being used to set up a print callback, leading to incorrect printing and failures.

Work towards having a working V1 -> V2 conversion for the release.

FYI @abdoo8080

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 04e8be64b14858a24a92678794497d88c015dcc1..7ba882f24ee52814c341c226f98d683e4f969840 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1267,7 +1267,8 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
         api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
 
         // make the let_body
-        api::Term body = applyParseOp(ops[i], largs);
+        std::vector<api::Term> largsApply = largs;
+        api::Term body = applyParseOp(ops[i], largsApply);
         // replace by lambda
         ParseOp pLam;
         pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body);