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 .
(bvurem s t)returns
tis 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 the
contrib/get-cadicalscript, 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.
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)