From d9bff0c0cd9a056e24d045f4de6912643d2db976 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 14 Apr 2018 09:14:07 -0500 Subject: [PATCH] Another fix for sygus rr stats. (#1768) --- src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 5 ++--- 1 file 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 -- 2.30.2