search

OCamlPro / alt-ergo

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

Invalid assumptions in array model generation #1212

Open bclement-ocp opened 3 weeks ago

bclement-ocp commented 3 weeks ago

Alt-Ergo crashes with an assertion failure in the union-find module with the following input:

; 1212.smt2
(set-logic ALL)
(set-option :produce-models true)
(declare-const a (Array Int Int))
(declare-const b (Array Int Int))
(assert (= (store a 0 0) (store b 0 0)))
(check-sat)
(get-model)

Using 0d6300ec27446ea57626a19dc0a7b00a80daf3a7 (current next at the time of writing):

$ alt-ergo 1212.smt2
; File "1212.smt2", line 7, characters 1-12: I don't know (0.0147) (8 steps) (goal g_1)

unknown
Fatal error: exception File "src/lib/reasoners/uf.ml", line 1276, characters 14-20: Assertion failed