В подобных случаях метод sexpr класса Solver - ваш друг!
Вы запутались из-за крайне слабо типизированной привязки z3py. Вызов Reals возвращает несколько результатов, которые вы присваиваете одному элементу. То есть ваша переменная input теперь является списком, содержащим одну переменную. Это, в свою очередь, делает всю программу бессмысленной, поскольку вы можете наблюдать за собой:
from z3 import *
s = Solver()
input = Reals('input')
s.add(input >= -2, input <= 2)
print s.sexpr()
Это печатает:
(assert true)
(assert false)
Почему? Поскольку ваша переменная input является списком, и причудливые правила продвижения типов решили, что список больше или равен -2, но меньше 2. (Это совершенно бессмысленно, просто то, как работают привязки. Там нет рифмы или причины, почему так должно быть. Можно утверждать, что это должно сделать больше проверки типов и дать вам правильную ошибку. Но я отступаю.)
Чтобы решить, просто измените свой вызов Reals на Real:
from z3 import *
s = Solver()
input = Real('input')
s.add(input >= -2, input <= 2)
print s.sexpr()
print s.check()
print s.model()
Это напечатает:
(declare-fun input () Real)
(assert (>= input (- 2.0)))
(assert (<= input 2.0))
sat
[input = 0]
, что именно то, что вы хотели сказать.