summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Expand)Author
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-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2020-12-15Remove bv divide by zero option (#5672)Andrew Reynolds
2020-12-11bv-to-int: new tests from an issue (#5654)yoni206
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-09Remove obsolete regressions (#5633)Andrew Reynolds
2020-11-30fix metadata for a test (#5546)yoni206
2020-10-16bv2int: caching introduced terms (#5283)yoni206
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-10-13bv2int: rewritings and unsat cores (#5263)yoni206
2020-09-23bv2int: new options for bvand translation (#5096)yoni206
2020-09-22Add simple BV solver (#5065)Mathias Preiner
2020-09-15bv2int: support models in tests (#5068)yoni206
2020-09-08Make CVC/API BV div/mod semantics match SMT-LIB (#4997)Andres Noetzli
2020-09-04[Regressions] Fix regression issues related to BV proofs (#5029)Haniel Barbosa
2020-09-03Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)Gereon Kremer
2020-08-28Incremental support for bv_to_int (#4967)yoni206
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-06-18Bv to int elimination bugfix (#4435)yoni206
2020-06-16Add missing REQUIRES to new regressions. (#4625)Aina Niemetz
2020-06-16BV: Fix querying equality status in lazy bit-blaster. (#4618)Aina Niemetz
2020-06-15BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)Aina Niemetz
2020-06-15BV: Add missing type check for INT_TO_BITVECTOR. (#4613)Aina Niemetz
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-24Int2BV fail on demand (#4079)yoni206
2020-03-09Enhancement: make the bool-to-bv pass more robust and targeted (#3021)makaimann
2020-02-24bv_to_int preprocessing passyoni206
2020-01-28Avoid PLUS with one child for bv2nat elimination (#3639)Andrew Reynolds
2019-12-16Support ackermannization on uninterpreted sorts in BV (#3372)Ying Sheng
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-12Refactor parser to define fewer tokens for symbols (#2936)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-05-15Fix model of Boolean vars with eager bit-blaster (#2998)Andres Noetzli
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
2018-12-10BoolToBV modes (off, ite, all) (#2530)makaimann
2018-12-06Enable BV proofs when using an eager bitblaster (#2733)Alex Ozdemir
2018-11-05Increasing coverage (#2683)yoni206
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-22Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)yoni206
2018-07-30Add support for incremental eager bit-blasting. (#1838)Mathias Preiner
2018-07-26Disabling bvLazyRewriteExtf in the right place (#2214)yoni206
2018-06-02Fix BV-abstraction check to consider SKOLEM. (#2042)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback