Clarify when to unfold defined constants
SMT-LIB allows custom defined constants with define-fun
. Currently it is unclear how the proofs for this have to look like.
If define-fun
defines a function, it is also necessary to clarify how the β-reduction is done.
This is also relevant for the option that introduces skolems as defined constants. In general this is relevant if we want to allow certain SMT-LIB commands within proofs which extend the signature.