diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-09-03 16:33:33 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-03 23:33:33 +0000 |
commit | 1eb3c6c8eb3da95cababcc0b1705c0299eee099c (patch) | |
tree | 72233917af15c553dfbbf59f1125952cab83c89b /src/preprocessing/passes/ite_simp.cpp | |
parent | 5cef06bd2beff38a911c74ec082d9789eed83421 (diff) |
EnvObj: Add options(), context(), userContext(). (#7137)
This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.
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) { |