From ce3a462918ac62c10b14d6a23be7e57db0ee984e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Dec 2021 13:10:05 -0600 Subject: [PATCH] Minor fix for sygus unsat query generator (#7811) --- src/theory/quantifiers/query_generator_unsat.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 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 -- 2.30.2