model validator reports error on valid model

[muchang]

Hi,
For this formula:

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< a 0))
(assert (= a (/ b c)))
(check-sat)
(get-model)

Z3 gives a valid model:

(model 
  (define-fun c () Real
    0.0)
  (define-fun b () Real
    1.0)
  (define-fun a () Real
    (- 1.0))
)

if model validator is enabled, it will report this valid model is invalid:

z3 model_validate=true file.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(model 
  (define-fun c () Real
    0.0)
  (define-fun b () Real
    1.0)
  (define-fun a () Real
    (- 1.0))
)

OS: Ubuntu 18.04
Revision: a78f899

[NikolajBjorner]

See #2663
They are all related to how /, mod, div, rem are dealt with.