Dumping internal define-funs with no arguments (#5077)

Dumping internal define-funs with no arguments (#5077)

Currently, --dump=assertions:... fails if a define-fun command is executed internally (an example for this can be found here.

The failure occurs because the printer expects a range type whenever a define-fun command is executed. However, when this command is used for 0-ary functions (variables), the getter for the range fails.

This PR fixes this by asking for a range only if the type is indeed a function. Otherwise, the original type is printed.

A test that currently fails but passes with this PR is included.