summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/candidate_rewrite_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.cpp')
-rw-r--r--src/theory/quantifiers/candidate_rewrite_database.cpp6
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 908bef92c..2d2e9ce30 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -276,11 +276,7 @@ CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen(
bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out)
{
- ExtendedRewriter* er = nullptr;
- if (options::synthRrPrepExtRew())
- {
- er = &d_ext_rewrite;
- }
+ ExtendedRewriter* er = &d_ext_rewrite;
Node nr;
if (er == nullptr)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback