diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 06f041d93..79bec60ee 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -562,7 +562,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Assert(vals.size() == candidates.size()); Node sbody = d_base_body.substitute( candidates.begin(), candidates.end(), vals.begin(), vals.end()); - Trace("cegis-sample-debug") << "Sample " << sbody << std::endl; + Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl; // do eager unfolding std::map<Node, Node> visited_n; sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index adc20008e..b95af719e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -458,11 +458,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Node lem; // introduce the skolem variables std::vector<Node> sks; + std::vector<Node> vars; if (constructed_cand) { if (inst.getKind() == NOT && inst[0].getKind() == FORALL) { - std::vector<Node> vars; for (const Node& v : inst[0][0]) { Node sk = nm->mkSkolem("rsk", v.getType()); @@ -527,10 +527,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Trace("cegqi-engine") << " * Verification lemma failed for:\n "; // do not send out - for (const Node& v : d_ce_sk_vars) + for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) { + Node v = d_ce_sk_vars[i]; Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); - Trace("cegqi-engine") << v << " -> " << mv << " "; + Trace("cegqi-engine") << vars[i] << " -> " << mv << " "; d_ce_sk_var_mvs.push_back(mv); } Trace("cegqi-engine") << std::endl; |