Unexpected exception thrown

[amenahh]

let y = Smtml.Typed.Float32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_fp 32) "y")

let expr =
  Smtml.Typed.Float32.neg
    (Smtml.Typed.Float32.add (Smtml.Typed.Float32.of_float 42.) y)

let expr = Smtml.Typed.Bitv32.reinterpret_f32 expr

let expr = Smtml.Typed.Bitv32.lt expr Smtml.Typed.Bitv32.one

module CVC5 = Smtml.Solver.Batch (Smtml.Cvc5_mappings)

let solver = CVC5.create ()

let () =
  match CVC5.check solver [ Smtml.Typed.Unsafe.unwrap expr ] with
  | `Sat -> Format.printf "SAT@\n"
  | `Unsat -> Format.printf "UNSAT@\n"
  | `Unknown -> Format.printf "UNKNOWN@\n"

For the following example an exception is thrown.
Z3 and Colibri2 return SAT

Here's the stack trace

Fatal error: exception Invalid_argument("expecting a bit-vector term")
Raised by primitive operation at Cvc5.Term.mk_term in file "cvc5.ml", line 98, characters 4-50
Called from Smtml__Mappings.Make.Make_.Encoder.encode_expr in file "src/smtml/mappings.ml", line 754, characters 16-33
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs.(fun) in file "src/smtml/mappings.ml", line 791, characters 27-44
Called from Stdlib__List.fold_left in file "list.ml", line 125, characters 24-34
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs in file "src/smtml/mappings.ml", lines 789-793, characters 10-24
Called from Smtml__Mappings.Make.Make_.Solver.check in file "src/smtml/mappings.ml", line 953, characters 40-76
Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
Called from Dune__exe__Bug8 in file "bug/bug8.ml", line 40, characters 8-60

[amenahh]

There's another exception thrown for the following code idk if it's linked to the previous bug. i can put this in another issue if you think it's unrelated

let y = Smtml.Typed.Float32.symbol (Smtml.Symbol.make (Smtml.Ty.Ty_fp 32) "y")

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

let expr =
  Smtml.Typed.Float32.rem
    (Smtml.Typed.Float32.of_float 7.3580)
    (Smtml.Typed.Float32.trunc y)

let expr = Smtml.Typed.Bitv32.reinterpret_f32 expr

let expr2 =
  Smtml.Typed.Bitv32.unsigned_rem (Smtml.Typed.Bitv32.of_int (-1925581473)) z

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

module CVC5 = Smtml.Solver.Batch (Smtml.Cvc5_mappings)

let solver = CVC5.create ()

let () =
  match CVC5.check solver [ Smtml.Typed.Unsafe.unwrap expr ] with
  | `Sat -> Format.printf "SAT@\n"
  | `Unsat -> Format.printf "UNSAT@\n"
  | `Unknown -> Format.printf "UNKNOWN@\n"

Z3 and Colibri2 return SAT

Here's the stack trace

Fatal error: exception Invalid_argument("Subexpressions must have the same type:\nEquation: (= false (bvurem #b10001101001110011111010101011111 z))\nType 1: Bool\nType 2: (_ BitVec 32)\n")
Raised by primitive operation at Cvc5.Term.mk_term in file "cvc5.ml", line 98, characters 4-50
Called from Smtml__Mappings.Make.Make_.Encoder.encode_expr in file "src/smtml/mappings.ml", line 754, characters 16-33
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs.(fun) in file "src/smtml/mappings.ml", line 791, characters 27-44
Called from Stdlib__List.fold_left in file "list.ml", line 125, characters 24-34
Called from Smtml__Mappings.Make.Make_.Encoder.encode_exprs in file "src/smtml/mappings.ml", lines 789-793, characters 10-24
Called from Smtml__Mappings.Make.Make_.Solver.check in file "src/smtml/mappings.ml", line 953, characters 40-76
Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
Called from Dune__exe__Bug7 in file "bug/bug7.ml", line 77, characters 8-60

[filipeom]

This is because cvc5 doesn't implement:

smtml/src/smtml/cvc5_mappings.default.ml

Line 504 in 214bee0

let to_ieee_bv = None

So it fallback into the default behaviour which is to create an uninterpreted function. However, cvc5 also currently doesn't expose ways to implement uninterpreted functions:

smtml/src/smtml/cvc5_mappings.default.ml

Lines 507 to 511 in 214bee0

	module Func = struct
	let make _ _ _ = ()
	let apply () _ = false_
	end

So when we call apply in:

smtml/src/smtml/mappings.ml

Line 420 in 214bee0

| 32 -> Func.apply f32_to_i32 [ t ]

It returns the false_ expression which is a boolean and fails later on. I'll see if with the current cvc5 API implemente the uninterpreted functions. Otherwise I'll have to submit a patch upstream to ocaml-cvc5

[filipeom]

Ok, turns out I need formalsec/ocaml-cvc5#47 to fix this