s Counterexamples for invalid model for Z3

Question

This is an extension of the question: Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?

In the below code, I am trying to use Z3 to get s counterexamples to a guess candidate for I satisfying some CHC clauses:

from z3 import *


x, xp = Ints('x xp') 

P = lambda x: x == 0
B = lambda x: x < 5
T = lambda x, xp: xp == x + 1
Q = lambda x: x == 5 

s = 10

def Check(mkConstraints, I, P , B, T , Q):
    s = Solver()
    # Add the negation of the conjunction of constraints
    s.add(Not(mkConstraints(I, P , B, T , Q)))
    r = s.check()
    if r == sat:
        return s.model()
    elif r == unsat:
        return {}
    else:
        print("Solver can't verify or disprove, it says: %s for invariant %s" %(r, I))

def System(I, P , B, T , Q):


    # P(x) -> I(x)
    c1 = Implies(P(x), I(x))

    # P(x) /\ B(x) /\ T(x,xp) -> I(xp) 
    c2 = Implies(And(B(x), I(x), T(x, xp)) , I(xp))

    # I(x) /\ ~B(x) -> Q(x)
    c3 = Implies(And(I(x), Not(B(x))), Q(x))

    return And(c1, c2, c3)


cex_List = []
I_guess = lambda x: x < 3


for i in range(s):
    cex = Check(System, I_guess, P , B , T , Q)
    I_guess = lambda t: Or(I_guess(t) , t == cex['x'])
    cex_List.append( cex[x] )

print(cex_List )

The idea is to use Z3 to learn a counterexample x0 for guess invariant I, then run Z3 to learn a counterexample for I || (x == x0) and so on till we get s counterexamples. However the following code gives 'RecursionError: maximum recursion depth exceeded '. I am confused because I am not even recursing with depth > 1 anywhere. Could anyone describe what's going wrong?