summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf
AgeCommit message (Expand)Author
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-06-05Fix handling of Boolean term variables (#4550)Andres Noetzli
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-03-21Fix various regression tests (#1657)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-11-17Fix Makefiles in testAndres Notzli
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-05Fixes some initialization and desctruction problems in quantifiers. Also rest...Tim King
2015-06-01When proof enabled, disable uf sym break. Add regression.ajreynol
2015-05-25Add missing regressionajreynol
2015-05-25Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.ajreynol
2015-04-21Fix file permissionsClark Barrett
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig...ajreynol
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes cas...Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions shou...Morgan Deters
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's m...Morgan Deters
2011-03-30improve recent low-coverage complaintsMorgan Deters
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-10-20fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug...Morgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-10additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supp...Morgan Deters
2010-09-28fix predicate bug in UF; code cleanup in theory.cppMorgan Deters
2010-09-02recategorize eq_diamond14 as a regress2 test (instead of regress0)Morgan Deters
2010-08-19UF theory bug fixes, code cleanup, and extra debugging output.Morgan Deters
2010-08-18more tests, configuration for UFMorgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
2010-07-04make dist && make distcheck functional, other fixesMorgan Deters
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback