summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Expand)Author
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-02Fix bv assert input reset assertions (#6820)Mathias Preiner
2021-06-30int-to-bv: correct model values (#6811)yoni206
2021-06-21Make CaDiCaL a required dependency. (#6761)Mathias Preiner
2021-06-10Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)Andrew Reynolds
2021-06-07(proof-new) Fix missing connection in trust substitution proofs (#6685)Andrew Reynolds
2021-06-04bv: Enable bitblast solver by default. (#6660)Mathias Preiner
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-06-02Fix unsat core proofs (#6655)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback