What additional axioms do we need to add so that Z3 can verify the satisfiability of programs with recurrences?

As we know Z3 has limitations with recurrences. Is there any way get the result for the following program? what will additional equation help z3 get the result?

    from z3 import *
    ackermann=Function('ackermann',IntSort(),IntSort(),IntSort())
    m=Int('m')
    n=Int('n')
    s=Solver()
    s.add(ForAll([n,m],Implies(And(n>=0,m>=0),ackermann(m,n) == If(m!=0,If(n!=0,ackermann(m - 1,ackermann(m,n - 1)),If(n==0,ackermann(m - 1,1),If(m==0,n + 1,0))),If(m==0,n + 1,0)))))
    s.add(n>=0)
    s.add(m>=0)
    s.add(Not(Implies(ackermann(m,n)>=0,ackermann(m+1,0)>=0)))
    s.check()