summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2014-03-20Merge pull request #22 from kbansal/sets-modelKshitij Bansal
2014-03-20cleanupKshitij Bansal
2014-03-20fix for sets/mar2014/..317minimized..Kshitij Bansal
2014-03-20Fix for registration issues of term appearing in a shared lemmaKshitij Bansal
2014-03-20fix a sharing issues with setsKshitij Bansal
2014-03-20enable check-models for sets/ regressionsKshitij Bansal
2014-03-20testlemma regressionsKshitij Bansal
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
2014-03-12Fix LogicInfo unit test.Morgan Deters
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback