Use Z3 solver to find `x` in `√x + √(x+15) = 15`

sqrt.py

# -*- coding: utf-8 -*-

from z3 import *

SOLVER = Solver()

# √x
Y = Real("Y")
X = Y * Y
SOLVER.add(Y > 0.0)

# √(x+15)
K = Real("K")
SOLVER.add(K > 0.0)
SOLVER.add(K * K == (X + RealVal("15.0")))

# √x + √(x+15) = 15
SOLVER.add( Y + K == RealVal("15") )

m = SOLVER.check()
if m == sat:
    print(SOLVER.model())
else:
    print("Cannot solve")