From 044fb6315119e0ad2f1ce57354f72d20ff4c6dc7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Oct 2018 00:34:16 -0500 Subject: [PATCH] Fix rewrite rule filtering. (#2591) --- src/theory/quantifiers/candidate_rewrite_database.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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& 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); } -- 2.30.2