Bug: SMTLIB2 formatted output does not contain Recursive Function definitions #7331
Description
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