[feature request] output only necessary bindings

[sorawee]

In recent versions of Z3, the produced models additionally contain bindings that correspond to define-fun inputs. As an example:

(declare-fun c0 () Bool)
(declare-fun c1 () Bool)
(define-fun e2 () Bool (and c0 c1))
(assert e2)
(check-sat)
(get-model)

used to produce (in Z3 4.8.8)

sat
(model
  (define-fun c0 () Bool
    true)
  (define-fun c1 () Bool
    true)
)

but now produces (in Z3 4.12.5)

sat
(
  (define-fun c0 () Bool
    true)
  (define-fun c1 () Bool
    true)
  (define-fun e2 () Bool
    (and c0 c1))
)

The new behavior also diverges from other solvers, like cvc5.

If I understand correctly, these extra bindings are a feature, not a bug. Still, would it be possible to add a flag to explicitly turn the feature on -- that is, to prune these extra bindings away by default unless the flag is on? Or if that's not possible, having a flag to switch to the old format would work too.

Our tool (Rosette) relies on the old format, and while we can make a solver-specific hack to make solvers compatible, we would prefer not to do that -- ideally all solvers (and across versions) should follow the same format.

[NikolajBjorner]

set smtlib2_compliant=true if you don't already. Then I omit adding macros and recursive functions to the model. Hope that helps.