summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-05Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.ajreynol
2014-11-05Merge branch '1.4.x'Morgan Deters
2014-11-05Fix get-bug-attachments script.Morgan Deters
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not assi...ajreynol
2014-11-01Added cache to getModelValueClark Barrett
2014-11-01Fix cegqi for synthesis without syntax.ajreynol
2014-11-01Simplify which lemmas to communicate in dt.ajreynol
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-31Do not allow duplication of function definitions. Set incomplete flag in mod...ajreynol
2014-10-30Be more lazy about generating array lemmasClark Barrett
2014-10-29Added new, much faster, care graph computation for arraysClark Barrett
2014-10-28Preprocessing step for finding finite runs of well-defined function definitio...ajreynol
2014-10-28Initial infrastructure for function definition quantifiers, internal parsing ...ajreynol
2014-10-28Improve stats in conjecture generator, minor cleanup.ajreynol
2014-10-25Minor fix for --user-pat=resortajreynol
2014-10-24Fix typo.Morgan Deters
2014-10-24Minor parser performance fix.Morgan Deters
2014-10-24Add --user-pat=resort. Minor cleanup of options.ajreynol
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-23Fixed inefficiency in bit-vector rewrite rule.lianah
2014-10-22Fix bug590 regression distcheck failure from last night.Morgan Deters
2014-10-21Fixed bug 589Tianyi Liang
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-20Minor cleanup in datatypes.ajreynol
2014-10-19Merge pull request #59 from kbansal/sets3Kshitij Bansal
2014-10-19Finish sets type enumerator implementation.Kshitij Bansal
2014-10-19fix statistic in decision engineKshitij Bansal
2014-10-18Fix assertion.ajreynol
2014-10-18Add dt lemma: zero size implies nullary constructor.ajreynol
2014-10-18Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi...ajreynol
2014-10-17Merge branch '1.4.x'Morgan Deters
2014-10-17Remove a bad (unstable, timing-dependent) test.Morgan Deters
2014-10-17Minor change for performance according to Andy's suggestion.Tianyi Liang
2014-10-16Fix clang warningsMorgan Deters
2014-10-16Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch...ajreynol
2014-10-16Merge branch '1.4.x'Morgan Deters
2014-10-16Add Thomas Hunger to THANKS file (for having submitted patches).Morgan Deters
2014-10-16Use n-ary splits instead of binary splits in theory datatypes.ajreynol
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by CE...ajreynol
2014-10-14fix for memory leak in BVQuickChecklianah
2014-10-14Merge pull request #58 from mdeters/smt-attributesMorgan Deters
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, a...Morgan Deters
2014-10-14amend prvs commitKshitij Bansal
2014-10-14trace decision-nodeKshitij Bansal
2014-10-13CEGQI uses model. Enforce fairness in CEGQI natively.ajreynol
2014-10-13Model building into quantifiers engine. Simplify axiom-inst mode.ajreynol
2014-10-13Refactor model builder from model engine to quant engine. Work on fairness s...ajreynol
2014-10-11Merge branch '1.4.x'Morgan Deters
2014-10-11Some defensive programming at destruction time, and fix a latent dangling poi...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback