Fixes a bug with arithmetic's new attempt solution infrastructure. This caused arith...

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 9db56ff682fcb78ec2b9fa56da907c83f2bf5ed2..f0cecc24b0e5f37a68be132bd257b71f1002e686 100644 (file)
--- 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;