Fix soudness bug in Enum

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo

https://alt-ergo.ocamlpro.com/

Other

130 stars 33 forks source link

Fix soudness bug in Enum #1091

Closed Halbaroth closed 4 months ago

Halbaroth commented 4 months ago

The PR #1078 introduces a soundness bug in assume_distinct. We have to propagate explanations of singleton domains, otherwise we may raise Inconsistency with an empty explanation.

Add a test that caught the bug.