Minor improvement to sygus trace (#2675)

1 files changed, 4 insertions, 3 deletions

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;