summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements to...ajreynol
2014-11-09Merge branch '1.4.x'Morgan Deters
2014-11-09Work around an apparent bug in libc++ that was causing crashes on Mac..Morgan Deters
2014-11-09Fix a deterministic assignment-ordering for get-assignment (fixes a regressio...Morgan Deters
2014-11-09Increase stack size when running regressions (fixes some regression crashes o...Morgan Deters
2014-11-09Fix dt shared terms issue, reenable regression.ajreynol
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression bug48...ajreynol
2014-11-08Merge pull request #62 from mdeters/bv-cleanupMorgan Deters
2014-11-07Remove some unused variables.Morgan Deters
2014-11-07Fixed bug in model builder with subtypesClark Barrett
2014-11-07Remove some dead code.Morgan Deters
2014-11-07Fix a memory leak in SatSolverRegistry (re: bug #594).Morgan Deters
2014-11-07Fix memory issues in bitvector theory, which is now valgrind-clean (mostly re...Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Corrected fix for missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr...ajreynol
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
2014-11-07Update competition build rules.Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
2014-11-07Fix missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-06Minor fix for getInstConsajreynol
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory com...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback