summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
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
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-22Fix bug590 regression distcheck failure from last night.Morgan Deters
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-17Merge branch '1.4.x'Morgan Deters
2014-10-17Remove a bad (unstable, timing-dependent) test.Morgan Deters
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, a...Morgan Deters
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti...Kshitij Bansal
2014-10-06Fix unit test that was broken with last commit.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-06Extended parsing testcase, with constant arrays and RESET.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ...Morgan Deters
2014-10-04Enable some old bug testcases that (maybe?) never got added.Morgan Deters
2014-10-03Add some (so far trivial) regressions for constant arrays.Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix unit test for ArrayStoreAll.Morgan Deters
2014-09-25fix unit test for new fair datatype enumerationMorgan Deters
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback