From: Tim King <taking@cs.nyu.edu>
Date: Tue, 2 Apr 2013 18:51:06 +0000 (-0400)
Subject: Making arithmetic model reversion on unsat checks an option.
X-Git-Tag: cvc5-1.0.0~7336
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de93aad21f843d54d02d0304343dffcb36dc2e09;p=cvc5.git

Making arithmetic model reversion on unsat checks an option.
---

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();