diff options
Diffstat (limited to 'src/preprocessing/passes/ite_simp.cpp')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 54e2b657e..434256d28 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -144,16 +144,17 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) } // Do theory specific preprocessing passes - if (d_env.getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH) + if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH) && !options::incrementalSolving()) { if (!simpDidALotOfWork) { util::ContainsTermITEVisitor& contains = *(d_iteUtilities.getContainsVisitor()); - arith::ArithIteUtils aiteu(contains, - d_preprocContext->getUserContext(), - d_preprocContext->getTopLevelSubstitutions().get()); + arith::ArithIteUtils aiteu( + contains, + userContext(), + d_preprocContext->getTopLevelSubstitutions().get()); bool anyItes = false; for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { |