Wrong solution for constraint involving addition
Description
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
Details
Assignee
Michael LeuschelReporter
Michael LeuschelPriority
MajorCreated October 30, 2020 at 3:36 PM
Updated September 22, 2021 at 10:59 AM
>>> :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