summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2010-05-21Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real....Tim King
2010-05-20Added the division symbol to the parser, and minimal support for it in Theory...Tim King
2010-05-19Significant revision to theory/arith. The new draft has a lot of small bug f...Tim King
2010-05-14Adding ITE testsChristopher L. Conway
2010-05-14Adding rudimentary ITE handling in CnfStreamChristopher L. Conway
2010-05-03more reasonable smt 2.0 benchmark testMorgan Deters
2010-05-03main driver supports .smt2 input, added an smt2 regression (currently broken,...Morgan Deters
2010-05-02smt parser for bit-vectorsDejan Jovanović
2010-04-04* Addressed issues brought up in Chris's review of Morgan'sMorgan Deters
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-12Fixing unnecessary construction of NOT nodes when generating conflict clause...Dejan Jovanović
2010-03-11Changing const TNode& to TNode in the CNF conversion + a new small benchmark ...Dejan Jovanović
2010-03-11Added some hand generated UF tests. Unfortunartely all of them work. Also fix...Tim King
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in t...Dejan Jovanović
2010-03-10Adding preliminary let/flet support to SMT parser (Bug #51)Christopher L. Conway
2010-03-09Adding support for "distinct" builtin in SMT parserChristopher L. Conway
2010-03-09Adding the smallest of test cases from the smtlib.Dejan Jovanović
2010-03-09removing makefile.inDejan Jovanović
2010-03-09one more simple test for ufDejan Jovanović
2010-03-09(no commit message)Dejan Jovanović
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-02-22resolve bug 32; public-facing interface functions in expr package must set cu...Morgan Deters
2010-02-11Adding precedence regressionsChristopher L. Conway
2010-02-09Changes to the CNF conversion and the SAT solver. All regression pass now, an...Dejan Jovanović
2010-02-06Preliminary support for types in parserChristopher L. Conway
2010-02-04assign expected-status to regressionsMorgan Deters
2010-02-04build system for multi-level regressionsMorgan Deters
2010-02-04Moved regressions into various levels based on running time.Tim King
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback