Unexpected exception thrown

[amenahh]

let a = Smtml.Expr.symbol (Smtml.Symbol.make Smtml.Ty.Ty_bool "a")

let expr = Smtml.Expr.Bool.implies a Smtml.Expr.Bool.true_

module Altergo = Smtml.Solver.Batch (Smtml.Altergo_mappings)
let solver = Altergo.create ()

let () =
  match Altergo.check solver [ 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.

[hra687261]

It would be helpful to add the error message/raised exception (and maybe even the stack_trace) to the issue.

[amenahh]

Here's the stack trace

Fatal error: exception Failure("Altergo_mappings: ae_expr_to_dvalue(@a0)")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Smtml__Altergo_mappings.M.Make.Solver.mk_model.(fun) in file "src/smtml/altergo_mappings.default.ml", line 203, characters 30-51
Called from Stdlib__Map.Make.fold in file "map.ml", line 329, characters 19-42
Called from Smtml__Altergo_mappings.M.Make.Solver.check in file "src/smtml/altergo_mappings.default.ml", line 222, characters 22-41
Called from Smtml__Utils.run_and_time_call in file "src/smtml/utils.ml", line 7, characters 15-19
Called from Dune__exe__Bug2 in file "smt/bug2.ml", line 29, characters 8-37

[hra687261]

Thanks!

[hra687261]

This should no longer be reproducible with alt-ergo's next branch commit ce48f8, but since that branch uses a newer unreleased version of dolmen, to use it we'd have to pin alt-ergo and dolmen in smtml (which will potentially require a substantial change since dolmen API changed a lot), alternatively we can add the fix to a branch of alt-ergo (2.6.x) that uses the released version of dolmen, which would make pinning from smtml simpler.
wdyt @redianthus @amenahh ?

[redianthus]

Well, I think we can simply wait for next release of Alt-Ergo and Smt.ml to be updated. :)