Dear SMT community,
I teach my MSc students about the many virtues of SMT solvers and advantages of their algebraic reasoning, but recently students come back asking me about the surprising limitations in bitvector reasoning, in particular when it comes to properties that carry over from the fact that bitvectors are integers modulo 2^N and thus many algebraic laws do carry over, even if conditionally.
For example, I am trying the following example
(set-logic QF_UFBV)
(declare-fun a () (_ BitVec 32))
(declare-fun b1 () (_ BitVec 32))
(declare-fun b2 () (_ BitVec 32))
(assert (and (bvslt #b00000000000000000000000000000000 a)
(bvslt #b00000000000000000000000000000000 b1)
(bvsle b1 b2)
(bvsgt (bvsdiv a b2) (bvsdiv a b1))))
(check-sat)
which arises from trying to prove:
def divAntimonotonic(a: Int, b1: Int, b2: Int) : Unit = {
require(0 < a && 0 < b1 && b1 <= b2)
()
} ensuring(_ => a / b2 <= a / b1)
I suppose that this is not in the library of standard BV pre-processing rewrites because it is a conditional fact that only works for positive b1,b2 ?
Are you aware of any solver options or nightly versions that would work on this smt2 file? cvc4 1.8 and z3 4.8.10 with default core seem to both time out?
Thanks,
Viktor