diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-14 09:14:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-14 09:14:07 -0500 |
| commit | d9bff0c0cd9a056e24d045f4de6912643d2db976 (patch) | |
| tree | 75f54854cf9836a86e525e194d9621f1cc637331 | |
| parent | 1bba8bcace3505cc9a3ba7d0cda6339c00217595 (diff) | |
Another fix for sygus rr stats. (#1768)
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 046c5724e..d160581bf 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -628,8 +628,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation rrChecker.assertFormula(crr.toExpr()); Result r = rrChecker.checkSat(); Trace("rr-check") << "...result : " << r << std::endl; - if (r.asSatisfiabilityResult().isUnknown() - || r.asSatisfiabilityResult().isSat()) + if (r.asSatisfiabilityResult().isSat()) { Trace("rr-check") << "...rewrite does not hold for: " << std::endl; @@ -652,7 +651,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation } else { - verified = true; + verified = !r.asSatisfiabilityResult().isUnknown(); } } else |