search

xapantu / counting-smt

1 stars 1 forks source link

Wrong result (sat instead of unsat) #9

Closed dddejan closed 8 years ago

dddejan commented 8 years ago

There is no u's that satisfy the constraints, therefore #{u} can not be > 0.

(set-logic QF_LIA)

(assert (> (# u Int 
 (and 
   (<= 0 u) (<= u 10)
   (or (< u 0) (> u 10))
 ))
 0
))

(check-sat)
xapantu commented 8 years ago

Already fixed with the last commits.

xapantu commented 8 years ago

I have put more tests for > and < in examples/novars.smt.

dddejan commented 8 years ago

Oops, sorry. Forgot to recompile.