summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2014-05-16sets: fix a bug in model building, another in handling set of setsKshitij Bansal
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-05-12Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.Tianyi Liang
2014-05-10Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m...Andrew Reynolds
2014-04-30T-entailment work, and QCF (quant conflict find) work that uses it.Tim King
2014-04-29fix was compiler warning in antlr_input, crashing test case with the old fixKshitij Bansal
2014-04-29add leading zeros support for str.to.intTianyi Liang
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-28travis, please!Kshitij Bansal
2014-04-27attempt to improve CVC4's "parse error" messageKshitij Bansal
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-09add testsKshitij Bansal
2014-04-09inputs to trigger bugKshitij Bansal
2014-04-06Reduced example from pcc's bug report.Tim King
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-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-28add construles, type_rules rm redundant, kinds cleanupKshitij Bansal
2014-03-27adds new feature: re.loopTianyi Liang
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-16Fix for ite of >=64bit wide bitvectors with unconstrained condition.Peter Collingbourne
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback