You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(set-logic HORN)
(declare-fun P (Int Int Int) Bool)
(declare-fun Q (Int Int) Bool)
(declare-fun R (Int Int Int) Bool)
(assert (forall ((x Int) (y Int) (z Int))
(=> (and (Q x y) (= z 0) (<= 1 y))
(P x y z))))
(assert (forall ((x Int) (y Int) (z Int))
(=> (and (R 1 z y) (= x 0)) (Q x y))))
(assert (forall ((x Int) (y Int) (z Int))
(=> (and (>= x (+ y))) (R x y z))))
(check-sat)
(get-model)
(exit)
Hello,
For this instance
z3 returns
If we take z <= 1, x = 0 in second clause, R(1, z, y) in this interpretation and x = 0 will be true but Q is false.
The text was updated successfully, but these errors were encountered: