Making arithmetic model reversion on unsat checks an option.

diff --git a/src/theory/arith/options b/src/theory/arith/options
index 129175eaff2380b64217ac685ad95298b6ce147c..87278fa61acd5b5bf31e5cd3762c381ad6909bc5 100644 (file)
--- 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 8c31c02ac7327731518b435cb765f4e56efc67b8..bc7b4b278f04531b959d2d5d9b693897ecb383df 100644 (file)
--- 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();