Invalid model on QF_UF formula false positive

[wintered]

The following traces shows a false positive in Z3's model validator. The returned model should be correct. Removing the (push) makes the bug disappear.

[639] % z3 model_validate=true small.smt2
sat
[640] % z3 rewriter.flat=false model_validate=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
[641] % 
[641] % cat small.smt2
(declare-fun a () Int)
(declare-fun b (Int) Bool)
(declare-fun c (Int) Bool)
(push)
(assert (or (or (not (b a)) (not (c a))) (c a)))
(assert (c (- a 1)))
(assert (= (c 0) (b 0)))
(assert (b (mod a (- 1))))
(check-sat)
[642] %

OS: Ubuntu 18.04
Commit: 5c9fd90

[NikolajBjorner]

arith.solver=2 provides correct model

[levnach]

Cannot repro it in 3cae0b4