| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(resolves bug #548).
|
|
|
|
|
|
|
|
|
|
final options/logic are set.
|
|
|
|
|
|
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
|
|
|
|
|
|
|
|
|
|
Some new functionality in substitutions.h/cpp
|
|
|
|
|
|
|
|
allows linearization of div,mod,/ by a constant.
|
|
|
|
|
|
quantification. Minor update to casc script.
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
removing an ugly forward declaration that was needed to get error set bound information on basic variables.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
