Bug: SMTLIB2 formatted output does not contain Recursive Function definitions

[AnirudhNarsipur]

from z3 import *
MList = Datatype('MList')
MList.declare('nil')
MList.declare('cons', ('head', IntSort()), ('rest', MList))
MList = MList.create()

listlen = RecFunction('listlen', MList, IntSort())
l1 = Const("l1", MList)
RecAddDefinition(listlen, l1, If( l1 == MList.nil, 0, 1 + listlen(MList.rest(l1))))

t1 = MList.cons(IntVal(10),MList.cons(IntVal(20),MList.nil))

s=Solver()
s.add(listlen(t1) == 2)
s.check() #SAT
print(s.to_smt2())

The above Python file prints:

; benchmark generated from python API
(set-info :status unknown)
(declare-datatypes ((MList 0)) (((nil) (cons (head Int) (rest MList)))))
 (assert
 (= ((_ listlen 0) (cons 10 (cons 20 nil))) 2))
(check-sat)

The output does not contain the definition for the listlen function making the smtlib output incomplete. Ideally the output should include the definition of the function:

; benchmark generated from python API
(set-info :status unknown)
(declare-datatypes ((MList 0)) (((nil) (cons (head Int) (rest MList)))))
(define-fun-rec listlen ((ls (MList))) Int
	(if (= ls nil)
		0
		(+ 1 (listlen (rest ls)))))

 (assert
 (= ((_ listlen 0) (cons 10  (cons 20 nil))) 2))
(check-sat)

Z3 Version: 4.13.0 64 bit
Python version : 3.10
OS: macOS 14.5