diff options
author | Tim King <taking@cs.nyu.edu> | 2015-06-14 00:51:19 +0200 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2015-06-14 00:51:30 +0200 |
commit | d101e7fed051685673c13317cb45166ba5ef7798 (patch) | |
tree | db2b64bba30ef2209a97b12f410a27c0a5e88786 /src/theory/arith/arith_ite_utils.cpp | |
parent | 16955c76a25a8030dc24840e74d0ab24d54f0a35 (diff) |
Turning off aggressive arith ite simplifications during incremental solving.
Diffstat (limited to 'src/theory/arith/arith_ite_utils.cpp')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 757dab8fb..2b31831e2 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -15,6 +15,7 @@ ** \todo document this file **/ +#include "smt/options.h" #include "theory/arith/arith_ite_utils.h" #include "theory/arith/normal_form.h" #include "theory/arith/arith_utilities.h" @@ -272,6 +273,7 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){ } Node ArithIteUtils::applySubstitutions(TNode f){ + AlwaysAssert(!options::incrementalSolving()); return d_subs->apply(f); } @@ -285,6 +287,7 @@ Node ArithIteUtils::selectForCmp(Node n) const{ } void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){ + AlwaysAssert(!options::incrementalSolving()); for(size_t i=0, N=assertions.size(); i < N; ++i){ collectAssertions(assertions[i]); } |