Invalid model for an incremental instance (default & 4.8.8 regression)

[muchang]

Hi,
For this case, Z3 gives an invalid model:

[721] % z3-4.8.8 model_validate=true small.smt2
sat
[722] % z3release model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
[723] % 
[723] % cat small.smt2
(declare-fun a () Real)
(assert (> (/ (* a a) (* 2 a)) 2))
(push)
(check-sat)
[724] %

OS: Ubuntu 18.04
Commit: a14c2a3

[levnach]

Works in ccda9d5