Invalid model was generated on Real formula #2811
Description
Hi,
consider the following formula.
(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ((c Real)) (or (<= 0 c) (> b a))))
(assert (= b (/ b a)))
(check-sat)
(get-model)
Z3 with model_validate=true returns a correct model but reports that that model is invalid.
sat
(error "line 5 column 10: an invalid model was generated")
(model
(define-fun a () Real
0.0)
(define-fun b () Real
(/ 1.0 8.0))
OS: Ubuntu 18.04
Revision: 49b6d5b