search

OCamlPro / alt-ergo

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

Add test from issue 1008 #1211

Closed Halbaroth closed 3 weeks ago

Halbaroth commented 4 weeks ago

This commit adds a test suggested by Basile in issue #1008.

bclement-ocp commented 3 weeks ago

I think we should also add the failing:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

And we would expect it to get fixed in #1211.

Halbaroth commented 3 weeks ago

Rofl, I forgot to call make promote.