#!/usr/bin/python3

from z3 import *

s=Solver()

x=Int("x")
base=Int("base")

#s.add(x>0)
#s.add(base>0)
s.add(base>=-20)
s.add(base<=20)
s.add(x*x == 1*base*base + 2*base + 1)

#print (s.check())
#print (s.model())

# enumerate all possible solutions:
results=[]
while True:
    if s.check() == sat:
        m = s.model()
        print (m)

        results.append(m)
        block = []
        for d in m:
            c=d()
            block.append(c != m[d])
        s.add(Or(block))
    else:
        print ("results total=", len(results))
        break