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

1 files changed, 4 insertions, 0 deletions

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;