summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2016-03-21New version of the recursive options parsing strategy.Tim King
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Removing dead code. StackingMap only appeared in unit tests.Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-30Shuffling around public vs. private headersTim King
2015-12-26Merged my changes from experimental branch (new array decision procedure,Clark Barrett
2015-12-24Miscellaneous fixesTim King
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback