Clarification of Quantifier Behaviour

[QMechanic]

Hello, sorry to disturb you with what might be a fairly trivial misunderstanding, but I have encountered some strange behaviour while using quantifiers that I do not understand, and would appreciate if someone could explain what I'm doing wrong.

I have this piece of code:

from z3 import *
def max(a, b):
    return If(a > b, a, b)

s = Solver()
x0, x1, x2, x3 = Ints("x0 x1 x2 x3")
s.add(x1 == max(x0-1, x2-1))
s.add(x2 == max(x1-1, x3-1))
s.add(x3 == max(x2-1, 0))

s.add(Exists([x0], (x0 >= 4) != (x3 >= 1))) ## sat
# s.add((x0 >= 4) != (x3 >= 1)) ## unsat
# s.add(ForAll([x0], (x0 >= 4) == (x3 >= 1))) ## unsat

status = s.check()
if status == sat:
    m = s.model()
    print(m)
else:
    print(status)

also the same code but in SMT2 format if you prefer reading that:

(declare-fun x2 () Int)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x3 () Int)
(assert (= x1 (ite (> (- x0 1) (- x2 1)) (- x0 1) (- x2 1))))
(assert (= x2 (ite (> (- x1 1) (- x3 1)) (- x1 1) (- x3 1))))
(assert (= x3 (ite (> (- x2 1) 0) (- x2 1) 0)))
(assert (exists ((x0 Int)) (distinct (>= x0 4) (>= x3 1)))) ; sat
(assert (distinct (>= x0 4) (>= x3 1))) ; unsat
(assert (forall ((x0 Int)) (= (>= x0 4) (>= x3 1)))) ; unsat

How is it possible for the exists quantifier to be satisfiable? It should intuitively be false as far as I can tell, and z3 confirms that assumption if I try to find an actual instance of x0 where the body is true.

I would also assume the forall quantifier to be satisfiable, but not according to z3. Am I fundamentally misunderstanding the semantics of quantifiers?

If someone could explain what I'm doing wrong that would be great. Thanks in advance.

[ThomasHaas]

Your quantifier "overwrites" the variable x0, i.e., it uses a fresh x0 variable that has no constraints associated.

(assert (exists ((x0 Int)) (distinct (>= x0 4) (>= x3 1)))) ; sat
// is effectively equal to
(assert (exists ((y Int)) (distinct (>= y 4) (>= x3 1)))) ; sat
// which is trivially sat (and the forall version is obviously unsat)

This query

(assert (distinct (>= x0 4) (>= x3 1))) ; unsat

is the correct "existential" query where all variables are constrained as intended (note that all variables are implicitly existentially quantified in sat queries).

[QMechanic]

Alright, is there any way to make the ForAll work as intenden though without re-defining every single variable to only depend on x0, creating quite a huge expression?
I'm wondering if it would be possible to have both constants that remain unchanged for all values that x0 can inhabit, as well as something like local temporary variables that are only used inside the quantifier body, such that I can apply the assertion without generating a huge expression.