GitLab

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) returns s if t 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 the contrib/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)