summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-03Add regression from #50 regarding "as" parsing in smt2 (#1188)Andrew Reynolds
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-10-01Refactor check function in last call effort of non-linear extension. (#1175)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Simplify representation of inversion Skolems for bv cegqi (#1164)Andrew Reynolds
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-25Fix bug related to sort inference + subtypes. (#1125)Andrew Reynolds
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-18Fix issue #1105 involving string to int (#1112)Andrew Reynolds
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
2017-09-13Add isConst check for lambda expressions. (#1084)Andrew Reynolds
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-30Fix model construction for parametric types (#1059)Andrew Reynolds
2017-08-14Build and test suite fixes for Windows (#186)Mark Laws
2017-08-08Use cache for datatypes cycle check, add regression.ajreynol
2017-08-07Optionally split regression tests into test groups (#207)Andres Noetzli
2017-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
2017-07-29Add support for charat in native language, minor cleanup.ajreynol
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ...ajreynol
2017-07-10Add nl regression.ajreynol
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-05Fix for logic info, update regressions. Update casc tfa script.ajreynol
2017-07-05Non-linear supported in ALL logics. Minor fixes for set logic with sygus.ajreynol
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, cbqi...ajreynol
2017-06-28Enable non-linear solve by default, update regressions.ajreynol
2017-06-22Fix assertion failure due to missing clause id (#180)Andres Nötzli
2017-06-21Properly handle subtypes in smt2 printer.ajreynol
2017-06-16Merge pull request #170 from CVC4/fix_2_6_parser3Clark Barrett
2017-06-16Fix segfault by making unit conflict CDMaybeAndres Nötzli
2017-06-16Parse 'is', 'match' differently for non-DT inputAndres Noetzli
2017-06-15Fix for bug 639.Clark Barrett
2017-06-15Add regression.ajreynol
2017-06-02Fix regression.ajreynol
2017-06-02Incorporate datatypes into smt comp script, add regression.ajreynol
2017-05-31Fix model construction for BV with cbqi. Minor change to defaults.ajreynol
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-05-26Checking that equalities belong to the arithmetic theory in the solve() routine.Tim King
2017-05-20Fix bug 812.ajreynol
2017-05-15Cleanup handling of division (possible fix for bugs 803, 804, 805).ajreynol
2017-05-15Merge pull request #158 from 4tXJ7f/fix_sets_rewriterAndrew Reynolds
2017-05-15Fix minor bug in sets rewriterAndres Noetzli
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.ajreynol
2017-05-10Do not split on cardinality for string equivalence classes with non-constant ...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback