OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Assertion failed in `Expr` on `next` #1099

Closed Halbaroth closed 2 months ago

Halbaroth commented 4 months ago

The next branch raises an assertion on 23 tests of our internal benchmark set. We should fix this issue before releasing the next version of Alt-Ergo:

alt-ergo: option '--frontend': this option is deprecated and will be ignored in the next version
Fatal error: exception File "src/lib/structures/expr.ml", line 1707, characters 4-10: Assertion failed
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 389, characters 17-32
Called from AltErgoLib__Satml_types.Flat_Formula.make in file "src/lib/structures/satml_types.ml", line 626, characters 10-29
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Alt_ergo_common__Solving_loop.main.d_fe in file "src/bin/common/solving_loop.ml", line 1047, characters 6-1023