summaryrefslogtreecommitdiff
path: root/test/regress/regress1/fmf
AgeCommit message (Expand)Author
2021-11-02Improve syntax for fmf cardinality constraints (#7556)Andrew Reynolds
2021-10-21Make cardinality constraint a nullary operator (#7333)Andrew Reynolds
2021-10-20Do not make assumption about model for Boolean variables in FMF (#7407)Andrew Reynolds
2021-10-05Finish refactoring on option handlers (#7295)Gereon Kremer
2021-09-29Update the syntax for tuples in smt2 (#7265)Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-22Fix type enumeration for non first-class sorts in FMF (#6719)Andrew Reynolds
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-06-03Renaming pow2 to p2 in regression tests (#6675)yoni206
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-01-29[proof-new] Connecting new unsat cores (#5834)Haniel Barbosa
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2021-01-19Use arbitrary ground term assignment for sorts where isInterpretedFinite is t...Andrew Reynolds
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-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-06-02Do not handle universal quantification on functions in model-based FMF (#4226)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-08Added CHOOSE operator for sets (#4211)mudathirmahgoub
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-31Fix fmf benchmark (#4193)Andrew Reynolds
2020-03-31Fix strange bound regression (#4192)Andrew Reynolds
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality (#4...Andrew Reynolds
2020-02-03Fix corner case of empty domains in bounded fmf (#3690)Andrew Reynolds
2020-01-30Fix rep set increment for empty domains (#3682)Andrew Reynolds
2020-01-22Fix subtyping for instantiations where internal representatives are chosen (#...Andrew Reynolds
2020-01-04Fix finiteness check for bounded fmf (#3589)Andrew Reynolds
2019-09-18Decouple fmf-bound and finite-model-find (#3297)Andrew Reynolds
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
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-28 Fix for get constraints method in fmf-fun (#2399)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-07-24Improvements to sets + cardinality + quantifiers (#2200)Andrew Reynolds
2018-06-02Fix preinitialization pass for finite model finding (#2047)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-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback