From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 14 Apr 2018 14:14:07 +0000 (-0500)
Subject: Another fix for sygus rr stats. (#1768)
X-Git-Tag: cvc5-1.0.0~5150
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9bff0c0cd9a056e24d045f4de6912643d2db976;p=cvc5.git

Another fix for sygus rr stats. (#1768)
---

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