From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Dec 2021 19:10:05 +0000 (-0600)
Subject: Minor fix for sygus unsat query generator (#7811)
X-Git-Tag: cvc5-1.0.0~669
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce3a462918ac62c10b14d6a23be7e57db0ee984e;p=cvc5.git

Minor fix for sygus unsat query generator (#7811)
---

diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp
index ae7288080..40131ffaa 100644
--- a/src/theory/quantifiers/query_generator_unsat.cpp
+++ b/src/theory/quantifiers/query_generator_unsat.cpp
@@ -66,18 +66,19 @@ bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out)
   size_t checkCount = 0;
   while (checkCount < 10)
   {
-    Assert(!activeTerms.empty());
     // if we just successfully added a term, do a satisfiability check
     if (addSuccess)
     {
+      Assert(!activeTerms.empty());
       checkCount++;
       // check the current for satisfiability
       currModel.clear();
       // Shuffle active terms to maximize the different possible behaviors
       // in the subsolver. This is instead of making multiple queries with
       // the same assertion order for a subsequence.
-      std::shuffle(activeTerms.begin(), activeTerms.end(), Random::getRandom());
-      Result r = checkCurrent(activeTerms, out, currModel);
+      std::vector<Node> aTermCurr = activeTerms;
+      std::shuffle(aTermCurr.begin(), aTermCurr.end(), Random::getRandom());
+      Result r = checkCurrent(aTermCurr, out, currModel);
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
         // exclude the last active term