I'm trying to implement satisfiability checking of a regular expression by converting it into a first-order logic formula based on the following excerpt from Rex: Symbolic Regular Expression Explorer

The problem seems to be that the circular reference(?) of Acc1 in the last axiom makes it so that Z3 is not capable of terminating and returns with "unknown" after a considerable amount of time. This seems weird to me, since if I understand correctly the second arguments of Acc0 and Acc1 are used to guarantee termination by decreasing until reaching a value of 0.

In my case to avoid naming conflicts the goal string is named w instead of s.

Note: Z3 also fails to return "sat" when a satisfying value (eg. "cc") is asserted to w.

Edit: After realizing the need for patterns (underlined parts in the screenshot) I've added them. Sadly Z3 still times out trying to solve this problem. I've looked into strategies but haven't found any that seems to help. It would be great if there was a way to eliminate the quantified formulas with the help of pattern matching.

from z3 import *;

def hd(x):
    return SubString(x, 0, 1)

def tl(x):
    return SubString(x,1,Length(x)-1)

def phi(x):
    return And(
        x >= StringVal('a'),
        x <= StringVal('z')
    )

solver = Solver()

solver.set()

Number = Datatype('Number')
Number.declare('nil') # 0
Number.declare('s', ('prev', Number)) # 1 = s(0), 2 = s(s(0))...
Number = Number.create()
nil = Number.nil
s = Number.s

x = String('x')
y = Const('y', Number)
w = String('w')

Acc0 = Function('Acc0', StringSort(), Number, BoolSort()) # String X Number -> Bool
Acc1 = Function('Acc1', StringSort(), Number, BoolSort()) # String X Number -> Bool

ax0_0 = ForAll( x, Acc0(x,nil) == False , patterns=[Acc0(x,nil)]) # For all(x: Acc0(x, 0) -> False
ax0_1 = ForAll( [x, y], Acc0(x, s(y)) == # For all(x,(y: Acc0(x, s(y)) <=>
    And(    
        Not(x == StringVal('')),               #(x != '' AND
        phi(hd(x)), # 'a' <= head(x) <= 'z' AND
        Acc1(tl(x),y)   # Acc1( tail(x),(y)
    ),
    patterns=[Acc0(x, s(y))]
)

ax1_0 = ForAll( x, Acc1(x,nil) == (x == StringVal('')), patterns=[Acc1(x,nil)]) # For all(x: Acc1(x, 0) <=>(x == ''
ax1_1 = ForAll( [x, y], Acc1(x, s(y)) == # For all(x,(y: Acc1(x, s(y)) <=>
    Or(
        And(                           # (
            Not(x == StringVal('')),   #(x != '' AND
            phi(hd(x)), # 'a' <= head(x) <= 'z' AND
            Acc1(tl(x),y)  # Acc1(tail(x),(y)
        ),                             # )
        x == StringVal('')            # OR(x == ''
    ),
    patterns=[Acc1(x, s(y))]
)

solver.add(
    Acc0(w, s(s(nil))),
    ax1_1,
    ax1_0,
    ax0_1,
    ax0_0
)

print(solver.check())