This PR fixes a linearity issue in `bv_decide`'s bitblaster, caused by the fact that the higher order combinators `AIG.RefVec.zip` and `AIG.RefVec.fold` were not being properly specialised. Example benchmark `QF_BV/sage/app1/bench_1967.smt2`: - before: https://share.firefox.dev/4cE86It - after: https://share.firefox.dev/42L9chd |
||
|---|---|---|
| .. | ||
| BVDecide | ||
| BVDecide.lean | ||