From de93aad21f843d54d02d0304343dffcb36dc2e09 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 2 Apr 2013 14:51:06 -0400 Subject: [PATCH] Making arithmetic model reversion on unsat checks an option. --- src/theory/arith/options | 3 +++ src/theory/arith/theory_arith.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) 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(); -- 2.30.2