diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:10:05 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-12-14 19:10:05 +0000 |
commit | ce3a462918ac62c10b14d6a23be7e57db0ee984e (patch) | |
tree | fdeb8345a2b900c92858584c8203560737053128 | |
parent | e029a6ace6456008ab774776d5f74919eefc9529 (diff) |
Minor fix for sygus unsat query generator (#7811)
-rw-r--r-- | src/theory/quantifiers/query_generator_unsat.cpp | 7 |
1 files 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<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 |