summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes cas...Morgan Deters
2014-03-11Minor cleanup.Morgan Deters
2014-03-11Fix for (get-assignment), resolves bug 553.Morgan Deters
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu...Andrew Reynolds
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-03-05Revert "fix naming conflicts in benchmarks"Kshitij Bansal
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-28a new regular expression engine for solving both positive and negative member...Tianyi Liang
2014-02-26sorry for the missing fileTianyi Liang
2014-02-26bug fix (caused by merge), move cardinality option to expert optionTianyi Liang
2014-02-21add new theory (sets)Kshitij Bansal
2014-02-20fix makefileTianyi Liang
2014-02-20add more tests, and define int.to.str(NEGATIVE)=""Tianyi Liang
2014-02-20add two cases to the regression testTianyi Liang
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2014-02-10Fix build (some nonexistent files listed in Makefile)Morgan Deters
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out inst...Andrew Reynolds
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U...Andrew Reynolds
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2013-12-26new functions in stringsTianyi Liang
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-13cleanupMorgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-05disable substring in default modeTianyi Liang
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now wor...Morgan Deters
2013-12-04Remove a regression for which the portfolio takes forever (see bug 542).Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-03adds LB strategyTianyi Liang
2013-12-02Add test case for (previously resolved) bug 528.Morgan Deters
2013-12-02Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a s...Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-10-24Fix for bug515Clark Barrett
2013-10-21add a string test caseTianyi Liang
2013-10-20adds regular expression rangeTianyi Liang
2013-10-16adds fmf for stringsTianyi Liang
2013-10-15bug fix: string cache cleaningTianyi Liang
2013-10-14add another regexp testTianyi Liang
2013-10-14Adds Regular Expression support.Tianyi Liang
2013-10-11Adds regular expression support, it is actually CFL because of variables.Tianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback