Age | Commit message (Expand) | Author |
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 suc... | Morgan Deters |
2013-11-05 | fixed proof regression script and added a new uf test case | lianah |
2013-09-13 | Move some regress benchmarks around that took too long, other test cleanup. | Morgan Deters |
2013-07-24 | Regressions now checking models on unknown too. But quantifiers don't have t... | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
2013-04-30 | add decision_attributes.h for make dist | Kshitij Bansal |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters |
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters |
2012-11-10 | Change run-regression script to *additionally* run a second test with --check... | Morgan Deters |
2012-09-27 | * Rename SMT parts (printer, parser) to SMT1 | Morgan Deters |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot |
2012-04-06 | * Smt2 printer for datatypes | François Bobot |
2012-04-05 | Support to test the "dumper" mechanism in regressions (feeding dump output ba... | Morgan Deters |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |
2011-10-28 | proof regressions | Morgan Deters |
2011-05-13 | * fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio | Morgan Deters |
2011-04-23 | * reviewed BooleanSimplification, added documentation & unit test | Morgan Deters |
2011-04-23 | make run_regression script robust to DOS newlines :( | Morgan Deters |
2011-03-30 | improve recent low-coverage complaints | Morgan Deters |
2011-03-15 | small fixes for run_regression script to workaround bug in old mktemp, was ca... | Morgan Deters |
2011-03-14 | change to the run_regression script to better manage temporary files; hopeful... | Morgan Deters |
2010-11-16 | SmtEngine now fails with a ModalException if --incremental is not enabled | Morgan Deters |
2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp... | Morgan Deters |
2010-10-04 | fix gdb issues (at least for static builds); resolves bug 194 | Morgan Deters |
2010-08-20 | turn off extra-checking (which does extra theory-rewriter checking); it was e... | Morgan Deters |
2010-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters |
2010-07-04 | don't do extra-checking for all regressions; that's probably a bad default | Morgan Deters |
2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
2010-06-30 | Support for failing .smt and .smt2 regressions (and other examples with | Morgan Deters |
2010-05-27 | added the ability to add custom expected stdout, stderr, and exit codes to sm... | Morgan Deters |
2010-05-03 | main driver supports .smt2 input, added an smt2 regression (currently broken,... | Morgan Deters |
2010-04-04 | * Addressed issues brought up in Chris's review of Morgan's | Morgan Deters |
2010-04-04 | * Node::isAtomic() now looks at an "atomic" attribute of arguments | Morgan Deters |
2010-02-09 | Changes to the CNF conversion and the SAT solver. All regression pass now, an... | Dejan Jovanović |
2010-02-04 | fix run_regression script | Morgan Deters |
2010-02-04 | test infrastructure updated for multiple-level regressions | Morgan Deters |