How to represent a symbolic summation in Z3?

I'm trying to represent sum of integers from an integer a to an integer b of the form

\sum_{i=a}^b i

Of courese there is a closed form solution for this version, but in general I'd like to sum over expressions parameterized by i. I've currently tried to define a function symSum and described its behavior using universal quantifiers:

from z3 import *
s = Solver()
symSum = Function('symSum', IntSort(), IntSort(), IntSort())

a = Int('a')
b = Int('b')
s.add(ForAll([a,b],If(a > b,symSum(a,b) == 0,symSum(a,b) == a + symSum(a+1,b))))
x = Int('x')
s.add(x == symSum(1,5))
print(s.check())
print(s.model())

I have not gotten this code to terminate (I have only allowed it to run for a couple minutes at max though). Is this outside the capabilities of Z3?

EDIT: Looking into this a bit more I was able to use recursive functions to define this!

from z3 import *
ctx = Context()
symSum = RecFunction('symSum', IntSort(ctx), IntSort(ctx), IntSort(ctx))
a = Int('a',ctx)
b = Int('b',ctx)
RecAddDefinition(symSum, [a,b], If(a > b, 0, a + symSum(a+1,b)))
x = Int('x',ctx)

s = Solver(ctx=ctx)
s.add(symSum(1,5) == x)
print(s.check())
print(s.model())