Minor improvement to sygus trace (#2675)

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 06f041d93e2b197577bb62c2623d0bb1f2e998d1..79bec60eee4805684376d9d6e62142716451558e 100644 (file)
--- 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 adc20008ec150d0ef202c34c4581c3bea5a363b6..b95af719e05c6596f8bcca6f9f693a84c120a733 100644 (file)
--- 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;