model completion for datatypes?

[quickbeam123]

In Vampire's AVATAR mod Z3, we need every bool literal to get a definite value in a model, however, Z3 is refusing to decided on the following example.

;- z3 parameter: rewriter.expand_store_eq=1
;- z3 parameter: model.compact=1

(declare-datatypes ( (Nat 0) ) (
    ( ( zero ) ( s ( p Nat ) ) )
))

(declare-fun v () Bool)

(assert (= v (= (p zero) zero)))

(check-sat)
(get-model)
(get-value (v))

giving us

sat
(
  (define-fun v () Bool
    (= (p zero) zero))
)
((v (= (p zero) zero)))