From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 30 Mar 2020 15:46:45 +0000 (-0500)
Subject: Fix arguments to print callback (#4171)
X-Git-Tag: cvc5-1.0.0~3427
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49d7b510a992a7a84594a11a4aeefcbd3fc8d257;p=cvc5.git

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 04e8be64b..7ba882f24 100644
--- 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);