inconsistent behaviour

[amenahh]

we don't have the same result when we wrote a smt file with a negative argument for rotate_left and the equivalent in ocaml

here's the smtlib file

(declare-const y (_ BitVec 32))
(declare-const z (_ BitVec 32))


(assert (= ((_ rotate_left -1) y)  z) )

(check-sat)

(get-model)

and the Z3 error when try to run it

(error "line 5 column 32: rotate left expects one integer parameter")
sat
(
  (define-fun z () (_ BitVec 32)
    #x00000000)
  (define-fun y () (_ BitVec 32)
    #x00000000)
)

here's the ocaml code

let y = Smtml.Typed.Bitv32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_bitv 32) "y")
let z = Smtml.Typed.Bitv32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_bitv 32) "z")

let expr = Smtml.Typed.Bitv32.rotate_left (-1) y

let expr = Smtml.Typed.Bitv32.eq expr z 

Z3 and CVC5 return SAT
Colibri2 throws an exception

Fatal error: exception Invalid_argument("Z.extract: nonpositive bit length")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Z.extract in file "z.ml", line 389, characters 16-63
Called from Colibri2_theories_LRA__RealValue.Check.compute_ground in file "colibri2/theories/LRA/realValue.ml", line 496, characters 46-69
Called from Colibri2_theories_LRA__RealValue.Check.attach.f in file "colibri2/theories/LRA/realValue.ml", line 670, characters 12-30
Called from Colibri2_core__Egraph.Delayed.do_pending in file "colibri2/core/egraph.ml", line 1158, characters 16-39
Called from Colibri2_core__Egraph.Backtrackable.flush in file "colibri2/core/egraph.ml", line 1386, characters 4-24
Called from Colibri2_solver__Scheduler.protect_against_contradiction in file "colibri2/solver/scheduler.ml" (inlined), line 821, characters 8-12
Called from Colibri2_solver__Scheduler.run_one_step_fix_model in file "colibri2/solver/scheduler.ml", lines 895-901, characters 6-24
Re-raised at Colibri2_solver__Scheduler.run_one_step_fix_model in file "colibri2/solver/scheduler.ml", lines 895-901, characters 6-24
Called from Colibri2_solver__Scheduler.run_inf_step in file "colibri2/solver/scheduler.ml", line 1009, characters 8-41
Called from Colibri2_solver__Scheduler.run_inf_step in file "colibri2/solver/scheduler.ml", line 1019, characters 4-49
Called from Colibri2_solver__Scheduler.check_sat.(fun) in file "colibri2/solver/scheduler.ml", line 1064, characters 4-37
Called from Smtml__Colibri2_mappings.M.Make.Solver.check in file "src/smtml/colibri2_mappings.default.ml", line 199, characters 15-46
Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
Called from Dune__exe__Bug5 in file "bug/bug5.ml", line 36, characters 8-64

[redianthus]

@filipeom, I'm not sure what's going on for this one.
My guess is that maybe the signed int when going through Z3 API's is turned into an unsigned one and does not fail in this case, or maybe Z3 is rejecting negative numbers at parsing time and does not reject it when using the API?

I'd say the correct fix is to check this directly in Smt.ml when building the rotate_left expression, WDYT?

Another possibility would be to normalize the number modulo the bitwidth, but I'm not sure it's a good idea. (I think that's what Z3 ends up doing when going through the API without checking the number first?)

@hra687261 I also think this could be checked in Colibri2 in order to emit a better error message? For now it seems this is only Zarith who's catching the issue.

[filipeom]

I think in general SMT-LIB specifies rotate_left only takes positive numbers.

My guess is that maybe the signed int when going through Z3 API's is turned into an unsigned one and does not fail in this case, or maybe Z3 is rejecting negative numbers at parsing time and does not reject it when using the API?

Not sure, smt solvers tend to be very permissive and try to return a sensible answer when they encounter an error. So what you describe might be what they are doing but we would need to check. From the error it looks like it's being triggered here: https://github.com/Z3Prover/z3/blob/d9d3be959c7ffa961a5d002282a544b5b28e885e/src/ast/bv_decl_plugin.cpp#L603

There is also the possibility that both z3 and cvc5 support negative number rotations and only output an error in order to be compliant with SMT-LIB? I.e., have some spec tests that check for these error messages.

In any case, we could do some tests to check if the API's behaviour is sound when negative numbers are passed to the rotate operators and then take it from there. I don't really care about being SMT-LIB compliant if it restricts our reasoning arbitrarily.