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
; declare a relation leq, making it equivalent to <=
(declare-fun leq (Int Int) Bool)
(assert (forall ((x Int) (y Int)) (= (leq x y) (<= x y))))
; declare a relation tcLeq, which is equivalent to the transitive-closure of leq
(declare-fun tcLeq (Int Int) Bool)
(assert (forall ((x Int) (y Int)) (= (tcLeq x y) ((_ transitive-closure leq) x y))))
; assert the NEGATION of the expectation that whenever we have x <= y and y <= z, then tcLeq x z must hold
(assert (not (forall ((x Int) (y Int) (z Int)) (implies (and (<= x y) (<= y z)) (tcLeq x z)))))
(check-sat)
(get-model)
I'm expecting unsat as the answer. However, z3 says:
Given:
I'm expecting
unsat
as the answer. However, z3 says:But this is unsound:
leq
to be equivalent to<=
, which is goodtcLeq
different from(_ transitive-closure leq)
, which is outlawed in the benchmark with the second call toassert
on line 7.The text was updated successfully, but these errors were encountered: