Invalid model issue on default mode

[depted]

Greetings, we found that an invalid bug occurred on this instance.
We tried to make this instance as small as possible. We sincerely hope that our report would be helpful for the z3 team.

$ ./z3 ./small.smt2 model_validate=true
sat
(error "line 5 column 10: an invalid model was generated")

$ cat ./small.smt2
(declare-fun p (Int) Int)
(declare-fun k () Int)
(assert (= 1 (mod (mod (- k) (+ 1 (- (- 3)))) (+ 2 1))))
(assert (< (p 3) (p k)))
(check-sat)

Commit: a0f3727