Using a bitvector of size 128 produces a failure with CVC4
Hello Why3 team,
I wrote a simple program that includes a the module BV128, here:
module M
use bv.BV128
let a (x : int) : int = assert { x = 0 }; x
end
If I want to prove the assertion with CVC4 (why3 prove -P cvc4 f.mlw
), but CVC4 raises a High Failure
error "Parse Error: /tmp/why_c9215b_adta-T-aqtvc.smt2:21.23: expecting bit-vector term"
Z3 does not raise an error.
However, when I look at the drivers, it looks like there is no driver for BV of size > 64. I do not know if the lack of drivers is related or simply if CVC4 does not support bitvectors of size 128.
It is a little blocking since we would like to be able to use bitvectors of size 128 to check the overflow of the operations performed with BV64.