CVC4 for smtlib 2.6
Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
Yes, the semantics changed in version 2.6 [0].
(bvurem s t)
returnss
ift
is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run thecontrib/get-cadical
script, then configure with--cadical
) and then using the flags--bitblast=eager --bv-sat-solver=cadical
(eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)