Transitive-closures: Unsound result

[LeventErkok]

Given:

; 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:

sat
(
  (define-fun leq ((x!0 Int) (x!1 Int)) Bool
    (<= (+ x!0 (* (- 1) x!1)) 0))
  (define-fun tcLeq ((x!0 Int) (x!1 Int)) Bool
    (ite (and (= x!0 0) (= x!1 38)) false
      ((_ transitive-closure leq) x!0 x!1)))
)

But this is unsound:

• The returned model indeed correctly makes leq to be equivalent to <=, which is good
• But then it makes tcLeq different from (_ transitive-closure leq), which is outlawed in the benchmark with the second call to assert on line 7.