Invalid model issue on QF_SLIA

[whangdo]

Greetings, For this instance, an invalid bug occurred. 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 13 column 10: an invalid model was generated")

$ cat ./small.smt2
(declare-const x Int)
(declare-fun s () String)
(assert (not (= 1 (str.len (str.substr s (+ 1 1) (- (+ 1 1 1 1) (+ 1 1)))))))
(assert (= 1 (str.len (str.substr s 1 1))))
(assert (= 1 (str.len (str.substr s 0 1))))
(assert (<= (ite (<= (str.to_int s) (seq.last_indexof s s)) 0 (str.to_int (str.substr s 0 3))) 0))
(assert (> (- (str.len s) 1 1 (+ 1 1)) 0))
(assert (<= 0 (- x 1 1 1)))
(assert (> (- (str.len s) 1 1) 0))
(assert (str.in_re s (re.+ (re.range "0" "9"))))
(assert (not (= 0 (str.len s))))
(assert (= "0" (str.at (str.substr s (+ 1 1) (- (+ 1 1 1 1) (+ 1 (seq.last_indexof (str.from_int 0) s)))) 0)))
(check-sat)

commit version: 50717fb