Kodkod detects inconsistency in a set comprehension assignment

Description

For this constraint, the Kodkod backend returns the wrong result

Maybe the fact the set is empty is erroneously propagated to the outside.

Environment

None

Activity

Show:

Michael Leuschel November 11, 2020 at 5:48 PM

Issue should be fixed now in 7ab1bbe80217e83a07fd32525352f4352612ab00.

is_inconsistent_expression has been improved to ignore elem(.) informations.

Michael Leuschel November 11, 2020 at 5:30 PM

Yes, an even simpler predicate is this one:

Fixed

Details

Assignee

Reporter

Priority

Created November 11, 2020 at 5:29 PM
Updated November 11, 2020 at 8:52 PM
Resolved November 11, 2020 at 8:52 PM