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.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 3e613cde5..1b123393b 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -137,9 +137,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
// options as the SmtEngine we belong to, where we ensure that
// produce-models is set.
bool needExport = false;
- ExprManagerMapCollection varMap;
ExprManager em(nm->getOptions());
std::unique_ptr<SmtEngine> rrChecker;
+ ExprManagerMapCollection varMap;
initializeChecker(rrChecker, em, varMap, crr, needExport);
Result r = rrChecker->checkSat();
Trace("rr-check") << "...result : " << r << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback