summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf
AgeCommit message (Expand)Author
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-02Improve syntax for fmf cardinality constraints (#7556)Andrew Reynolds
2021-09-29Update the syntax for tuples in smt2 (#7265)Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
2021-03-08Fix handling of negation of Boolean bound variables in FMF (#6066)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-10-12Remove uf-ss-totality option (#5251)Andrew Reynolds
2020-09-11Move finite model minimization to UF last call effort (#5050)Andrew Reynolds
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-01-30Ensure literals in FMF decision strategies are in the CNF stream (#3669)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-28Fix sort inference for quantified variables of interpreted types (#2393)Andrew Reynolds
2018-08-17 Fix spurious warning in sort inference (#2331)Andrew Reynolds
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-04-05 Python regression script (#1662)Andres Noetzli
2018-03-23Add a few quantifiers regressions to improve coverage (#1702)Andrew Reynolds
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function defi...ajreynol
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-14Fix for fmf-fun when the option is set by user command.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-15Allow 0 argument recursive functions. Fixes bug 782.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership li...ajreynol
2017-01-11Fix for when variables are (partially) bound in multiple ways, add regression...ajreynol
2017-01-04Marking regression test files as non-executable.Tim King
2016-12-07Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.ajreynol
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback