diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-30 10:46:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-30 10:46:45 -0500 |
| commit | 49d7b510a992a7a84594a11a4aeefcbd3fc8d257 (patch) | |
| tree | 2c89f6cc19789a3d5b326e7d1b712bf677e67ec9 | |
| parent | 0060de329173c0b75c02778d003371f59cc11eff (diff) | |
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
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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); |