summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
AgeCommit message (Expand)Author
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
2014-08-18Revert a8e0ce67 and add test case (resolves bug #578).Morgan Deters
2014-08-04Some fixes to symmetry breaker (resolves bug 576).Morgan Deters
2014-07-12Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre f...Morgan Deters
2014-06-27Fix for bug543Clark Barrett
2014-06-19forgot to add the test with fixKshitij Bansal
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-08test for prvs commit (tokenize emptyset)Kshitij Bansal
2014-04-29fix was compiler warning in antlr_input, crashing test case with the old fixKshitij Bansal
2014-04-06Merge pull request #21 from pcc/ite-fixTim King
2014-04-03Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann...Morgan Deters
2014-03-16Fix for ite of >=64bit wide bitvectors with unconstrained condition.Peter Collingbourne
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-08Merge remote-tracking branch 'CVC4root/master'Tim King
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2014-03-07Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m...Tim King
2014-03-05Array smtlib compliance testsKshitij Bansal
2014-02-21add new theory (sets)Kshitij Bansal
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback