Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-11-29 | Improve caching in term formula removal (#1398) | Andrew Reynolds | |
2017-03-17 | better support for proof production when encountering bool terms: handle the ↵ | guykatzz | |
new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes | |||
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
2017-01-18 | Fix non-idempotent rewrite in Array rewriter | Andres Noetzli | |
This commit fixes bug 637 ( http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as proposed in Bugzilla and adds the minified test case to the regression tests. | |||
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. | |||
2014-11-08 | Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵ | ajreynol | |
bug484, enable parsing_ringer. | |||
2014-11-07 | Properly distinguish which EQC to assign values in datatypes, use ↵ | ajreynol | |
assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure. | |||
2014-10-06 | Extended parsing testcase, with constant arrays and RESET. | Morgan Deters | |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: test/regress/regress0/arrays/Makefile.am | |||
2014-10-06 | Fix native language parsing of chained-store expressions (resolves bug 585). ↵ | Morgan Deters | |
Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic. | |||
2014-10-04 | Enable some old bug testcases that (maybe?) never got added. | Morgan Deters | |
2014-10-03 | Add some (so far trivial) regressions for constant arrays. | Morgan Deters | |
2014-03-12 | Some standardization of regression Makefiles that got out of sync. Fixes ↵ | Morgan Deters | |
cases of nonterminating rewrite-rules regressions. | |||
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-09-18 | Support a personal build configuration and make rules. | Morgan Deters | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2012-08-28 | fix regression tests for automake 1.11 and automake 1.12---both versions ↵ | Morgan Deters | |
should work now | |||
2012-05-14 | Fixed assertion failures in array theory | Clark Barrett | |
This fixes bugs 335 and 333. | |||
2012-04-18 | add the missing BINARY variable in some test/regress makefiles | Kshitij Bansal | |
2012-04-11 | merge from arrays-clark branch | Morgan Deters | |
2012-04-05 | Support to test the "dumper" mechanism in regressions (feeding dump output ↵ | Morgan Deters | |
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump" | |||
2011-10-29 | support for proof regressions in other parts of the test tree | Morgan Deters | |
2011-07-12 | forgot to reflect naming change in makefile. fixed | Morgan Deters | |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters | |
2011-07-11 | remove some array regressions from "make check" so nightly regressions run | Morgan Deters | |
2011-07-11 | status of examples | Morgan Deters | |
2011-07-11 | new array bugs ? | Morgan Deters | |
2011-07-11 | mark the new minimized benchmark as unsat | Morgan Deters | |
2011-07-11 | if running in QF_AX, equalities over terms of uninterpreted sort go to ↵ | Morgan Deters | |
arrays, as well as pre-registration of free constants of uninterpreted sort, etc.. | |||
2011-07-11 | minimized example | Morgan Deters | |
2011-07-11 | array benchmarks | Morgan Deters | |
2011-05-23 | Merge from arrays2 branch. | Morgan Deters | |