Tree-order failures

[LeventErkok]

According to the guide (https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/), amongst other properties, a tree-order is reflexive, and satisfies:

 (assert (forall ((x A) (y A) (z A)) (=> (and (R x y) (R x z)) (or (R y z) (R z y)))))

Looks like both are failing in z3:

Reflexivity:

(declare-sort A 0)
(define-fun R ((x A) (y A)) Bool ((_ tree-order 0) x y))

(declare-const a A)
(assert (not (R a a)))
(check-sat)

This prints sat.

For the second axiom:

(declare-sort A 0)
(define-fun R ((x A) (y A)) Bool ((_ tree-order 0) x y))

(declare-const x A)
(declare-const y A)
(declare-const z A)
(assert (not (forall ((x A) (y A) (z A)) (=> (and (R x y) (R x z)) (or (R y z) (R z y))))))
(check-sat)

which also prints sat.

[NikolajBjorner]

Maybe a switcharound, the following is unsat

(declare-sort A 0)
(define-fun R ((x A) (y A)) Bool ((_ tree-order 0) x y))

(declare-const x A)
(declare-const y A)
(declare-const z A)
(assert (not (forall ((x A) (y A) (z A)) (=> (and (R y x) (R z x)) (or (R y z) (R z y))))))
(check-sat)
(exit)

[NikolajBjorner]

I checked the code again and concluded this is a documentation bug.
The intent is reversed of the documentation you cite. I have updated the documentation on z3guide.