diff options
| author | Tim King <taking@cs.nyu.edu> | 2013-04-02 14:51:06 -0400 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2013-04-02 15:06:48 -0400 |
| commit | de93aad21f843d54d02d0304343dffcb36dc2e09 (patch) | |
| tree | 8a07584e422f95d1b0416d7fdaba24cef765d6bd /src/theory | |
| parent | 166bbd9c5716e646769cdc38aaeff3bd75de94f8 (diff) | |
Making arithmetic model reversion on unsat checks an option.
Diffstat (limited to 'src/theory')
| -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(); |