search

xapantu / counting-smt

1 stars 1 forks source link

Wrong result #7

Closed dddejan closed 8 years ago

dddejan commented 8 years ago

From first assertion s1 = 2 From second assertion s2 = 1 From third assertion s3 = 0

Output I get is s3 = 2, s2 = 2, s1 = 2

(set-logic QF_LIA)

(declare-fun s1 () Int)
(declare-fun s2 () Int)
(declare-fun s3 () Int)

(assert (= s1 (# u Int (and (>= u 1) (>= 2 u)))))
(assert (= s2 (# u Int (and (>= u 1) (>= 2 u) (< u s1)))))
(assert (= s3 (# u Int (and (>= u 1) (>= 2 u) (< u s2)))))

(check-sat)
(get-model)
xapantu commented 8 years ago

Fixed when #6 was fixed.