Fix rewrite rule filtering. (#2591)

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index bba5b3c1869bf89eb7ca31cd547d969685929c5e..908bef92c6b246347773df6fcf5f7978469e7d87 100644 (file)
--- 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);
 }