Debug build spurious model validation error on arithmetic formula with rem (release build okay)

[zhendongsu]

Commit: 83e2e72
OS: Ubuntu 18.04

Not sure how relevant it is, but shown below is a spurious model validation failure from the debug build
(spurious since the model generated by the debug build is correct):

[571] % z3release model_validate=true small.smt2 
sat
[572] % z3debug model_validate=true small.smt2 
sat
(error "line 9 column 10: an invalid model was generated")
[573] % 
[573] % cat small.smt2 
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun f () Int)
(declare-fun h () Int)
(assert (= 0 (+ b (* c d))))
(assert (> (rem 0 (+ c (* a d))) f h (+ (* b f) (* c h)) 0))
(check-sat)
[574] % 

[NikolajBjorner]

I will not be fixing model evaluation bugs with "rem".
Rem is rewritten to "mod" by pre-processing, but evaluation does not rewrite it.
Instead it gets re-interpreted when the second argument is 0.
I would argue that the bug isn't interesting because it relates to models where the second argument to rem is 0, and there the interpretation of rem is not fixed. Reasonable uses of rem should constrain the scope of second arguments to non-zero to not rely on anomalies. Fuzz tools will invariably create test cases that don't correspond to what I postulate as reasonable, but there are more useful bugs/features to focus on.