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 ae7288080fa18806c9a8bf44eb2453797fa0fb0c..40131ffaaf1ec2347171a8afd091cb9315f4d24c 100644 (file)
--- 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