invalid model issue on an incremental QF_SLIA formula

[zhendongsu]

[578] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
(error "line 16 column 10: an invalid model was generated")
(
  (define-fun a () Bool
    false)
  (define-fun s () String
    "A200")
  (define-fun b () Int
    0)
)
[579] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Int)
(declare-fun s () String)
(push)
(assert (ite (str.prefixof "-" (str.substr s 1 (- 4 1))) (and (= 1 (str.to_int (str.substr s 1 (+ 1 1 1)))) (> (str.len (str.substr s 1 (- (+ 1 1 1 1) 1))) 1)) (not (= (- 1) (str.to_int (str.substr s 1 (- 4 1)))))))
(check-sat)
(push)
(assert (not (= (str.at (str.substr s 1 1) 0) "0")))
(check-sat)
(push)
(assert (not (= 1 (str.len (str.substr s 1 (- (+ 1 1 1 1) 1))))))
(check-sat)
(push)
(check-sat)
(assert (not (<= (ite a b (str.to_int (str.substr s 1 (- 4 1)))) 255)))
(check-sat)
(get-model)