From: Tim King <taking@cs.nyu.edu>
Date: Tue, 7 May 2013 18:38:46 +0000 (-0400)
Subject: Fixes a bug with arithmetic's new attempt solution infrastructure.  This caused arith... 
X-Git-Tag: cvc5-1.0.0~7287^2~146
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09813b6f7c68db999503af16ec53fbfb757e5665;p=cvc5.git

Fixes a bug with arithmetic's new attempt solution infrastructure.  This caused arithmetic to think it was in a conflict incorrectly. This lead to it not properly responding to new input and lead to an inconsistency bug.

This could be triggered previously by running:
./builds/bin/cvc4 --stats --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --new-prop --dio-decomps --unconstrained-simp --fancy-final /home/taking/benchmarks/smtlib2/QF_LRA/miplib/opt1217--17.smt2
---

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 9db56ff68..f0cecc24b 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -67,6 +67,7 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
 
   if(processSignals()){
     Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl;
+    d_conflictVariables.purge();
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
     Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl;
@@ -114,9 +115,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     bool conflict = processSignals();
     if(conflict){
       d_errorSet.reduceToSignals();
+      d_conflictVariables.purge();
+
       return Result::UNSAT;
     }
   }
+  Assert( d_conflictVariables.empty() );
 
   if(d_errorSet.errorEmpty()){
     return Result::SAT;