Fixes a bug with arithmetic's new attempt solution infrastructure. This caused arith...
authorTim King <taking@cs.nyu.edu>
Tue, 7 May 2013 18:38:46 +0000 (14:38 -0400)
committerTim King <taking@cs.nyu.edu>
Tue, 7 May 2013 18:38:46 +0000 (14:38 -0400)
commit09813b6f7c68db999503af16ec53fbfb757e5665
treee296f3ac386f72140bb253e99a18006207b63fc6
parentd5638ce2fc70625c2b0bbc013b37d96fb5306568
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
src/theory/arith/attempt_solution_simplex.cpp