Age | Commit message (Collapse) | Author |
|
for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is a bandaid for constraints-tempo-width family of benchmarks.
|
|
|
|
|
|
|
|
being pure virtual.
|
|
removing an ugly forward declaration that was needed to get error set bound information on basic variables.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* normalizing in bv before bitblasting
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|