| Age | Commit message (Expand) | Author |
|---|
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
| 2015-10-11 | fix regression tests, support fallback mode for proofs | Kshitij Bansal |
| 2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
| 2015-01-14 | sygus input language and benchmark | Morgan Deters |
| 2014-11-09 | Merge branch '1.4.x' | Morgan Deters |
| 2014-11-09 | Increase stack size when running regressions (fixes some regression crashes o... | Morgan Deters |
| 2014-07-21 | run_regression using valgrind by setting VALGRIND=1 | Kshitij Bansal |
| 2014-04-28 | travis, please! | Kshitij Bansal |
| 2014-03-07 | Fix run_regression on Mac. | Morgan Deters |
| 2014-03-05 | Array smtlib compliance tests | Kshitij Bansal |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
| 2013-12-13 | Fix stack size on in-tree regressions. | Morgan Deters |
| 2013-12-13 | Some minor cleanup. | Morgan Deters |
| 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 |
