Age | Commit message (Collapse) | Author | |
---|---|---|---|
2016-11-17 | Fix Makefiles in test | Andres Notzli | |
With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that. | |||
2016-10-21 | Move slow regress0 benchmarks to regress1, increment regress1 through regress3. | ajreynol | |
2014-02-09 | More complete guess instantiation strategy, cvc4 now typically times out ↵ | Andrew Reynolds | |
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc | |||
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-09-18 | Support a personal build configuration and make rules. | Morgan Deters | |
2013-09-13 | Move some regress benchmarks around that took too long, other test cleanup. | Morgan Deters | |
2013-08-26 | bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x | Kshitij Bansal | |
2013-08-26 | Bug 374 benchmarks | Kshitij Bansal | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2012-09-18 | SMT-LIBv2 compliance regarding outputting "unknown". | Morgan Deters | |
Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-08-28 | fix regression tests for automake 1.11 and automake 1.12---both versions ↵ | Morgan Deters | |
should work now | |||
2012-07-27 | Minor cleanup after today's commits: | Morgan Deters | |
* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning | |||
2012-07-16 | now passes "make distcheck", which does important checks for the release ↵ | Morgan Deters | |
(e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...) | |||
2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović | |
disableing one test case in equantifiers/decision that runs long | |||
2012-06-17 | Fix array bug causing incorrect answers | Clark Barrett | |
2012-06-16 | Adding the failing QF_AUFLIA regression mentioned in last commit. | Kshitij Bansal | |
pp-regfile.delta02.smt is the one to look at with --decision=justificaiton, the delta minimized version of pp-regfile, which also gives wrong answer. due to various commits/fixes, delta01 gives correct answer currently. | |||
2012-06-15 | one bug fixed | Kshitij Bansal | |
2012-06-14 | add failing regression, move error up | Kshitij Bansal | |
2012-06-14 | bug fixes in justification heuristic | Kshitij Bansal | |
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp | |||
2012-06-14 | enabling fixed bug345 case | Dejan Jovanović | |
2012-06-14 | fix quantifier non-bug | Kshitij Bansal | |
2012-06-14 | failing quantifier | Kshitij Bansal | |
2012-06-14 | add passing regression | Kshitij Bansal | |
2012-06-13 | add passing regression | Kshitij Bansal | |
2012-06-13 | enable some decision regressions | Kshitij Bansal | |
2012-06-13 | decision regressions, all but one fail | Kshitij Bansal | |