Wrong solution for constraint involving addition

Description

>>> :kodkod 2000 + x = y & 3000 + y : {10000,10001}
kodkod ok: 2000 + x = y & 3000 + y : {10000,10001} ints: irange(2000,10001), intatoms: irange(10000,10001)
Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).
Times for computing solutions: [222,26,28,20,18,25,23,13,12,12,9,10,9,11,10,10,11,8,9,7,11,11]
Existentially Quantified Predicate over x,y is TRUE
Solution:
x = 6204 &
y = 8204

Environment

None

Activity

Show:

Michael Leuschel September 22, 2021 at 10:59 AM

Other smaller and probably related issues are

Michael Leuschel October 30, 2020 at 3:37 PM

Obviously 3000+y is not in {10000,10001}

Details

Assignee

Reporter

Priority

Created October 30, 2020 at 3:36 PM
Updated September 22, 2021 at 10:59 AM