assert false in int modulo

[amenahh]

For the following example an exception is thrown.

let expr = Smtml.Typed.Int.mod_ (Smtml.Typed.Int.v 4) (Smtml.Typed.Int.v 2)  

let expr = Smtml.Typed.Int.eq expr (Smtml.Typed.Int.v 0) 

module Z3 = Smtml.Solver.Batch (Smtml.Z3_mappings)

let solver = Z3.create ()

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

Here's the stack trace

Fatal error: exception File "src/smtml/typed.ml", line 938, characters 28-34: Assertion failed
Raised at Smtml__Typed.Int.mod_ in file "src/smtml/typed.ml", line 938, characters 28-40
Called from Dune__exe__Bug6.expr in file "bug/bug6.ml", line 2, characters 11-75

[redianthus]

It looks like this one is simply not implemented:

  let[@inline] mod_ _x _y = assert false

[filipeom]

I'll open a PR for this soon.