summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2010-06-04Enabling RDL/IDL in SMT v1 and adding some simple testsChristopher L. Conway
2010-06-03Fixes 2 issues with assignments. The first is constructing an initial assignm...Tim King
2010-06-02more VERBOSE test failuresMorgan Deters
2010-05-29Adding a couple of example from fuzzsmt to regress1.Tim King
2010-05-27Reverting this file to not include any comments. (Morgan's revision and my re...Tim King
2010-05-27added the ability to add custom expected stdout, stderr, and exit codes to sm...Morgan Deters
2010-05-27Preregistration has been turned on. Highly experimental eager splitting suppo...Tim King
2010-05-27Use the newer automake test driver "parallel-tests". This driver:Morgan Deters
2010-05-27Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)Christopher L. Conway
2010-05-27fix bug 120; competition mode regression failures for intentionally-buggy inputMorgan Deters
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-08Fixing the test case, it had a unary or. The cnf converter should be adapted ...Dejan Jovanović
2010-02-06Preliminary support for types in parserChristopher L. Conway
2010-02-04fix run_regression scriptMorgan Deters
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
2010-02-03Adding functions/predicates to SMT grammarChristopher L. Conway
2010-02-03simple ITE parsingDejan Jovanović
2010-02-03Enabled more regress tests. Takes 26s on my machine to run a make -k check in...Tim King
2010-02-03some more tests for the context.Dejan Jovanović
2010-02-01Added this test back to avoid make check problems.Tim King
2010-01-29fixed CNF conversion, and more modular; CNF conversion command line option; v...Morgan Deters
2010-01-28Removing Makefile.in'sChristopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback