summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2015-04-21Fix file permissionsClark Barrett
2015-04-21Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.ajreynol
2015-04-21Adding an example of a tester in SMT2.Tim King
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-17Merge pull request #72 from kbansal/decision-requirephaseKshitij Bansal
2015-04-15Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2Tim King
2015-04-15Adding an example that violates an assertion during unconstrained simplificat...Tim King
2015-04-09disable string reqressions timing out after changeKshitij Bansal
2015-03-23Parsing support for define-fun-rec/define-funs-rec.ajreynol
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig...ajreynol
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-02-14Fix unit tests.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2015-02-05Minor clean upTianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2015-01-20Mark datatypes as sygus. Add option to normalize sygus terms in search. Add...ajreynol
2015-01-19Adding tests for get-value output for arithmetic.Tim King
2015-01-14sygus input language and benchmarkMorgan Deters
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2015-01-07bug fix, thanks to Pierre's reportTianyi Liang
2014-12-28Disable prenex by default when using fmf bound int, minor improvement to data...ajreynol
2014-12-04Relaxed the constant requirement for regular expression loop;Tianyi Liang
2014-12-03Floating point infrastructure.Martin Brain
2014-11-26add intersection rewritingTianyi Liang
2014-11-21Throw error when pattern is not list of terms.ajreynol
2014-11-21Change default option to --inst-when=full-last-call (interleave instantiation...ajreynol
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. Chang...ajreynol
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ho...ajreynol
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting theori...Dejan Jovanović
2014-11-09Merge branch '1.4.x'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-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-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-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-06Reenable regression. Add (for now, disabled) changes to datatypes theory com...ajreynol
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not assi...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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback