summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Expand)Author
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
2018-05-30Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)Mathias Preiner
2018-05-21Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)makaimann
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-20Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enab...yoni206
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Fix corner case for rewrite of mult by pow 2 (#1601)Andrew Reynolds
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-05-31Minor change to defaults, update smt comp script, minor changes to options in...ajreynol
2017-03-28Fix bug 787.ajreynol
2017-03-28Fix for bug 733Clark Barrett
2017-03-24Add some regressions. Minor.ajreynol
2017-01-05Disabling a regression test that assumes CVC4 is configured with proofs on. M...Tim King
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres Notzli
2016-12-02Fix for bug 734Clark Barrett
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres Notzli
2016-11-17Fix Makefiles in testAndres Notzli
2016-11-11Add simple inferences for extended bitvector functions, add a few related opt...ajreynol
2016-10-26Enable bv2nat regressionsajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2014-06-13fixed BVMinisat bug due to not clearing seen properlylianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes cas...Morgan Deters
2014-03-11Minor cleanup.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-04-26Merge experimental decisionweight branchKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback