diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-07 14:38:46 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-07 14:38:46 -0400 |
commit | 09813b6f7c68db999503af16ec53fbfb757e5665 (patch) | |
tree | e296f3ac386f72140bb253e99a18006207b63fc6 /src | |
parent | d5638ce2fc70625c2b0bbc013b37d96fb5306568 (diff) |
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
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/attempt_solution_simplex.cpp | 4 |
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; |