summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
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-07Fix run_regression on Mac.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-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
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-21Fix makefile dependence for system tests.Morgan Deters
2014-02-21disable test cvc3_main, attempt to fix dist_checkKshitij Bansal
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-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2013-12-26new functions in stringsTianyi Liang
2013-12-24Merge branch '1.3.x'Morgan Deters
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-18Add missing regression-results directory.Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-13Fix stack size on in-tree regressions.Morgan Deters
2013-12-13cleanupMorgan Deters
2013-12-13Some minor cleanup.Morgan Deters
2013-12-10Fix timer statistics to report correct time even on process abort.Morgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-05disable substring in default modeTianyi Liang
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
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-20Changing the number of bits allocated per field in node values.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback