projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Only allow bv2nat/int2bv with BV and integer logic (#4118)
[cvc5.git]
/
test
/
regress
/
regress0
/
bv
/
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
tree
|
commitdiff
2020-02-25
yoni206
bv_to_int preprocessing pass
tree
|
commitdiff
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
tree
|
commitdiff
2019-12-16
Ying Sheng
Support ackermannization on uninterpreted sorts in...
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-06-21
Andres Noetzli
Fix and simplify handling of --force-logic (#3062)
tree
|
commitdiff
2019-06-12
Andres Noetzli
Refactor parser to define fewer tokens for symbols...
tree
|
commitdiff
2019-06-04
Andres Noetzli
Add check that result matches benchmark status (#3028)
tree
|
commitdiff
2019-05-15
Andres Noetzli
Fix model of Boolean vars with eager bit-blaster (...
tree
|
commitdiff
2019-03-16
Alex Ozdemir
Enable CryptoMiniSat-backed BV proofs (#2847)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
tree
|
commitdiff
2018-11-05
yoni206
Increasing coverage (#2683)
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added regression tests and target make regress.
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-08-22
yoni206
Generating less consistency lemmas in bv-ackermann...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
tree
|
commitdiff
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
tree
|
commitdiff
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
tree
|
commitdiff
2018-05-21
makaimann
Handle IMPLIES in bool-to-bv and test it in regress0...
tree
|
commitdiff
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
tree
|
commitdiff
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
tree
|
commitdiff
2018-04-20
yoni206
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
tree
|
commitdiff
2018-03-21
Andres Noetzli
Move regression tests to single Makefile.am (#1658)
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Fix corner case for rewrite of mult by pow 2 (#1601)
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Refactor regressions (#1581)
tree
|
commitdiff
2018-02-06
Andrew Reynolds
Fix two multiply-by-constant corner cases for bv rewrit...
tree
|
commitdiff
2018-01-02
Andrew Reynolds
Rewrites for BitVector multiplication (#1465)
tree
|
commitdiff
2017-10-28
Andres Noetzli
Change bvudiv semantics based on input language (#1292)
tree
|
commitdiff
2017-05-31
ajreynol
Minor change to defaults, update smt comp script, minor...
tree
|
commitdiff
2017-03-29
ajreynol
Fix bug 787.
tree
|
commitdiff
2017-03-29
Clark Barrett
Fix for bug 733
tree
|
commitdiff
2017-03-24
ajreynol
Add some regressions. Minor.
tree
|
commitdiff
2017-01-05
Tim King
Disabling a regression test that assumes CVC4 is config...
tree
|
commitdiff
2017-01-04
Andrew Reynolds
Merge pull request #122 from 4tXJ7f/fix_lfsc_str
tree
|
commitdiff
2017-01-04
guykatzz
Merge pull request #120 from 4tXJ7f/fix_f_pp_holes
tree
|
commitdiff
2016-12-17
Andres Notzli
Fix dependency tracing for fewerPreprocessingHoles
tree
|
commitdiff
2016-12-03
Clark Barrett
Fix for bug 734
tree
|
commitdiff
2016-12-02
Tim King
Merge pull request #95 from 4tXJ7f/fix_sierra_build
tree
|
commitdiff
2016-12-02
Clark Barrett
Merge pull request #113 from 4tXJ7f/remove_extract_rule
tree
|
commitdiff
2016-11-30
Andres Notzli
Remove wrong `ExtractMultLeadingBit` rule
tree
|
commitdiff
2016-11-18
Clark Barrett
Merge pull request #110 from 4tXJ7f/fix_makefiles
tree
|
commitdiff
2016-11-18
Andres Notzli
Fix Makefiles in test
tree
|
commitdiff
2016-11-12
Tim King
Merge pull request #105 from timothy-king/delete-maxed-out
tree
|
commitdiff
2016-11-11
ajreynol
Add simple inferences for extended bitvector functions...
tree
|
commitdiff
2016-10-26
ajreynol
Enable bv2nat regressions
tree
|
commitdiff
2016-10-21
ajreynol
Move slow regress0 benchmarks to regress1, increment...
tree
|
commitdiff
2016-10-13
ajreynol
Merging bv parts of ajr/bvExt branch, minor additions...
tree
|
commitdiff
2016-01-27
Liana Hadarean
Merged bit-vector and uf proof branch.
tree
|
commitdiff
2014-06-13
lianah
fixed BVMinisat bug due to not clearing seen properly
tree
|
commitdiff
2014-06-10
lianah
Merging CAV14 paper bit-vector work.
tree
|
commitdiff
2014-04-01
Tim King
Merge branch '1.3.x'
tree
|
commitdiff
2014-03-26
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-03-21
Kshitij Bansal
Merge pull request #22 from kbansal/sets-model
tree
|
commitdiff
2014-03-12
Morgan Deters
Some standardization of regression Makefiles that got...
tree
|
commitdiff
2014-03-11
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-03-11
Morgan Deters
Minor cleanup.
tree
|
commitdiff
2014-03-11
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-02-21
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-02-21
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-02-19
Tim King
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-27
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-18
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-17
Kshitij Bansal
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-09
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-08
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2014-01-02
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2013-12-27
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2013-12-26
Tianyi Liang
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2013-12-24
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2013-12-24
Morgan Deters
Merge branch '1.3.x'
tree
|
commitdiff
2013-12-23
Morgan Deters
Proof-checking code; fixups of segfaults and missing...
tree
|
commitdiff
2013-11-11
Tianyi Liang
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2013-11-11
Morgan Deters
Change exit status to be more consistent with other...
tree
|
commitdiff
2013-09-30
Liana Hadarean
merged golden
tree
|
commitdiff
2013-09-18
Morgan Deters
Support a personal build configuration and make rules.
tree
|
commitdiff
2013-05-03
Tim King
Merging branch 'soiquickexplain'.
tree
|
commitdiff
2013-05-03
Tim King
Merge branch 'fcexplanations'
tree
|
commitdiff
2013-04-30
lianah
fixed merge conflicts
tree
|
commitdiff
2013-04-29
Kshitij Bansal
Merge pull request #9 from kbansal/master
tree
|
commitdiff
2013-04-26
Kshitij Bansal
Merge experimental decisionweight branch
tree
|
commitdiff
2013-03-29
Dejan Jovanović
Merge branch 'master' of github.com:CVC4/CVC4
tree
|
commitdiff
2013-03-27
lianah
Merge branch 'master' into bv-core
tree
|
commitdiff
2013-03-27
lianah
added model generation for bv subtheories and bv-inequa...
tree
|
commitdiff
2013-03-23
lianah
non-incremental inequality solver seems to be bug-free...
tree
|
commitdiff
2013-03-22
lianah
Merge branch 'master' into bv-core
tree
|
commitdiff
2013-03-21
lianah
Merge branch 'master' into bv-core
tree
|
commitdiff
2013-03-21
lianah
Merge branch 'master' into bv-core
tree
|
commitdiff
2013-03-21
lianah
added regression test for constant eval
tree
|
commitdiff
2013-03-21
lianah
Merge branch 'master' into bv-core
tree
|
commitdiff
2013-03-21
lianah
added more tests
tree
|
commitdiff
2013-03-21
lianah
generalized bv inequality reasoning to handle both...
tree
|
commitdiff
2013-03-20
Liana Hadarean
one more ineq regression
tree
|
commitdiff
2013-03-20
Liana Hadarean
fixed reversed concat in core theory
tree
|
commitdiff
2013-03-20
Liana Hadarean
merged master with dejan's constant evaluating equality...
tree
|
commitdiff
2013-03-20
Liana Hadarean
inequality reasoning works on small examples added...
tree
|
commitdiff
2013-03-16
lianah
started work on the inequality bv subtheory
tree
|
commitdiff
2013-03-15
Morgan Deters
Merge branch '1.0.x'
tree
|
commitdiff
next