diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arith/options | 3 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/arith/options b/src/theory/arith/options index 129175eaf..87278fa61 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -65,4 +65,7 @@ option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool : option maxCutsInContext --maxCutsInContext unsigned :default 65535 maximum cuts in a given context before signalling a restart +option revertArithModels --revert-arith-models-on-unsat bool :default false + Revert the arithmetic model to a known safe model on unsat if one is cached + endmodule diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 8c31c02ac..bc7b4b278 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1649,7 +1649,7 @@ void TheoryArith::check(Effort effortLevel){ break; case Result::UNSAT: d_unknownsInARow = 0; - if(previous == Result::SAT){ + if(options::revertArithModels() && previous == Result::SAT){ ++d_statistics.d_revertsOnConflicts; Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; revertOutOfConflict(); |