summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
AgeCommit message (Expand)Author
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-10-16Fix for issue 1247 (#1257)Clark Barrett
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-09-25Fix bug related to sort inference + subtypes. (#1125)Andrew Reynolds
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ...ajreynol
2017-06-16Merge pull request #170 from CVC4/fix_2_6_parser3Clark Barrett
2017-06-16Parse 'is', 'match' differently for non-DT inputAndres Noetzli
2017-06-15Fix for bug 639.Clark Barrett
2017-04-21Disabled bug639.smt2 which still fails.Clark Barrett
2017-04-21Add test cases for bugs 639 and 681.Clark Barrett
2017-04-05Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-01-10Adding regression test scrubbing.Tim King
2016-11-30Fix parsing of BVROTR by CVC parserAndres Notzli
2016-11-17Fix Makefiles in testAndres Notzli
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2015-09-04Fix bugs 605 and 667.ajreynol
2015-08-19fix bug 605Kshitij Bansal
2015-07-27Disable bug590.smt2Tianyi Liang
2015-04-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm...ajreynol
2015-01-19Adding tests for get-value output for arithmetic.Tim King
2015-01-14sygus input language and benchmarkMorgan Deters
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting theori...Dejan Jovanović
2014-11-09Fix dt shared terms issue, reenable regression.ajreynol
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug48...ajreynol
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Corrected fix for missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-01Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemma...ajreynol
2014-11-01Fix some mistakes in datatypes theory combination, disable two regressions. ...ajreynol
2014-10-22Fix bug590 regression distcheck failure from last night.Morgan Deters
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti...Kshitij Bansal
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ...Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback