smt - Why does Z3 return unknown for this nonlinear integer arithmetic example? -

i have simple example in nonlinear integer arithmetic, namely search pythagorean triples. based on read in related questions (see below), i'd expect z3 find solution problem, returns 'unknown'. here example in smt-lib v2:

(declare-fun x () int) (declare-fun y () int) (declare-fun z () int) (declare-fun xsquared () int) (declare-fun ysquared () int) (declare-fun zsquared () int) (declare-fun xsquaredplusysquared () int)  (assert (= xsquared (* x x))) (assert (= ysquared (* y y))) (assert (= zsquared (* z z))) (assert (= xsquaredplusysquared (+ xsquared ysquared)))  (assert (and (> x 0) (> y 0) (> z 0) (= xsquaredplusysquared zsquared)))  (check-sat)  (exit) 

---

there few related questions, notably:

• how z3 handle non-linear integer arithmetic?

• need understanding equation

• combining nonlinear real linear int

• z3 support nonlinear arithmetic

• z3 limitations in handling nonlinear real arithmetics

it seems z3 won't attempt finding solution bit-blasting unless variables have finite range. replacing (check-sat) following command find solution:

(check-sat-using (then (using-params add-bounds :add-bound-lower -100 :add-bound-upper 100) smt)) 

alternatively, 1 can add assert statements forcing each variable have finite range.