Age | Commit message (Expand) | Author |
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 |