Make sygus infer find function definitions (#1951)

[cvc5.git] / src / theory / quantifiers / candidate_rewrite_database.cpp

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index fc7ec8e5242d356886cd67c86484a3093d419884..03c39f718947d1e8b87113a73dd1b6a053608a77 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -105,7 +105,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
         rrChecker.assertFormula(crr.toExpr());
         Result r = rrChecker.checkSat();
         Trace("rr-check") << "...result : " << r << std::endl;
-        if (r.asSatisfiabilityResult().isSat())
+        if (r.asSatisfiabilityResult().isSat() == Result::SAT)
         {
           Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
           success = false;