From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 5 Oct 2018 05:34:16 +0000 (-0500)
Subject: Fix rewrite rule filtering. (#2591)
X-Git-Tag: cvc5-1.0.0~4455
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=044fb6315119e0ad2f1ce57354f72d20ff4c6dc7;p=cvc5.git

Fix rewrite rule filtering. (#2591)
---

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index bba5b3c18..908bef92c 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -64,7 +64,7 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
   d_qe = qe;
   d_tds = d_qe->getTermDatabaseSygus();
   d_ext_rewrite = nullptr;
-  d_crewrite_filter.initialize(ss, d_tds, false);
+  d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
   ExprMiner::initialize(vars, ss);
 }