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 046c5724e174c9fd1242e9aad4f8a8db91f7551e..d160581bfbc9eb87745c9eea5655d55d434d5d0a 100644 (file)
--- 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