summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2015-04-27Updating failing unit tests.Tim King
2015-02-14Fix unit tests.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2014-12-03Floating point infrastructure.Martin Brain
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-17Merge branch '1.4.x'Morgan Deters
2014-10-17Remove a bad (unstable, timing-dependent) test.Morgan Deters
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, a...Morgan Deters
2014-10-06Fix unit test that was broken with last commit.Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix unit test for ArrayStoreAll.Morgan Deters
2014-09-25fix unit test for new fair datatype enumerationMorgan Deters
2014-08-22Unit test fix.Morgan Deters
2014-08-04Better support for resource-limiting when there aren't any actual conflicts.Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-25BinaryHeap unit test and some usability/build fixes for the data structure it...Morgan Deters
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-21fixed build failurelianah
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-11Merge pull request #31 from kbansal/setsKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-06-11disable failing testKshitij Bansal
2014-05-27update stats_blackKshitij Bansal
2014-04-01Merge branch '1.3.x'Tim King
2014-04-01Fixing bug 552. There was a bug when integers are made using a string with a...1.3.xTim King
2014-03-12Fix LogicInfo unit test.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-10Fix timer statistics to report correct time even on process abort.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-02Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a s...Morgan Deters
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-11Theory of strings.Tianyi Liang
2013-09-09Add support for check-sat with argument.Morgan Deters
2013-06-27Remove output.h from public space, to avoid clashes with symbols defined in u...Morgan Deters
2013-06-04Merge branch '1.2.x'Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-03Fixing compilation of unit tests. These problems were due to splitLemma() bei...Tim King
2013-04-05Fix unit test (compile error) for new SatSolver interfaceMorgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback