Invalid model issue

[whangdo]

Greetings, For this instance, an invalid model bug occurred. We checked other issues on string theory(#6857, #6907). These instances do not trigger invalid model bugs anymore on the current commit version. Therefore, we think that our instance triggers another cause different from the past bugs. Also, we tried to minimize the instance however, we failed to reduce the size of this instance. Even though the size of this instance is not small, we truly hope that this instance will be helpful for the z3 team.

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

$ cat ./small.smt2
(set-logic ALL)
(declare-fun s () String)
(declare-fun generated_1 () String)
(assert (not ( = ( str.len ( str.substr s ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( - ( str.len s  ) ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  )  )  )  ) 1  )))
(assert ( <= ( ite ( str.prefixof "-" ( str.substr s ( + 1 ( + 1 1  )  ) ( - ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( + 1 ( + 1 1  )  )  )  )  ) ( - ( str.to_int ( str.substr ( str.substr s ( + 1 ( + 1 1  )  ) ( - ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( + 1 ( + 1 1  )  )  )  ) 1 ( - ( str.len ( str.substr s ( + 1 ( + 1 1  )  ) ( - ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( + 1 ( + 1 1  )  )  )  )  ) 1  )  )  )  ) ( str.to_int ( str.substr s ( + 1 ( + 1 1  )  ) ( - ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( + 1 ( + 1 1  )  )  )  )  )  ) 255  ))
(assert (ite (str.prefixof "-" (str.substr s (+ 1 (+ 1 1)) (- (+ (+ 1 (+ 1 1)) (+ (+ 1 1) 1)) (+ 1 (+ 1 1))))) (and (ite (= (- 1) (str.to_int (str.substr (str.substr s (+ 1 (+ 1 1)) (- (+ (+ 1 (+ 1 1)) (+ (+ 1 1) 1)) (+ 1 (+ 1 1)))) 1 (- (str.len (str.substr s (+ 1 (+ 1 1)) (- (+ (+ 1 (+ 1 1)) (+ (+ 1 1) 1)) (+ 1 (+ 1 1))))) 1)))) false true) (> (str.len (str.substr s (+ 1 (+ 1 1)) (- (+ (+ 1 (+ 1 1)) (+ (+ 1 1) 1)) (+ 1 (+ 1 1))))) 1)) (>= 0 (seq.last_indexof s s))))
(assert (not ( = ( str.at ( str.substr s ( + 1 ( + 1 1  )  ) ( - ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( + 1 ( + 1 1  )  )  )  ) 0  ) "0"  )))
(assert (not (= (str.len (str.++ (str.replace (str.substr (str.substr (str.replace s "9" s) (str.to_code s) (+ 12 0)) (div (ite true 255 12) (* 255 1)) (seq.last_indexof (ite false s "-") (str.replace "-" "0" s))) (ite (<= (str.to_int s) (seq.last_indexof "0" "-")) (ite (str.suffixof s generated_1) (str.++ "-" "9") (str.replace s s "9")) (str.replace (ite false "9" s) (ite true s "9") (ite false s "-"))) (str.++ (str.substr (str.substr "0" 12 12) (abs 0) (- 3 1)) (str.replace (str.replace "0" s s) (ite false s "-") (str.at "-" 0)))) (str.replace (str.++ (str.replace (str.++ "0" "-") (str.replace "9" s "0") "-") (str.replace s (str.++ s s) (str.at "-" 1))) (str.from_int (str.len s)) (str.replace (str.from_code 3) (str.at (str.substr "0" 255 0) (str.indexof "0" "-" 12)) (str.at (str.at s 1) (* 12 0)))))) 1)))
(assert ( <= ( ite ( str.prefixof "-" ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) ( - ( str.to_int ( str.substr ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  ) 1 ( - ( str.len ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) 1  )  )  )  ) ( str.to_int ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  )  ) 255  ))
(assert ( ite ( str.prefixof "-" ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) ( and ( ite ( = (- 1) ( str.to_int ( str.substr ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  ) 1 ( - ( str.len ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) 1  )  )  )  ) false true  ) ( > ( str.len ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) 1  )  ) ( ite ( = (- 1) ( str.to_int ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  )  ) false true  )  ))
(assert (not ( = ( str.at ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  ) 0  ) "0"  )))
(assert (not ( = ( str.len ( str.substr s 1 ( - ( + 1 ( + 1 1  )  ) 1  )  )  ) 1  )))
(assert ( = ( str.len ( str.substr s 0 ( - 1 0  )  )  ) 1  ))
(assert ( <= ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) 3  ))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) 0  ))
(assert (not ( <= ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) ( + 1 1  )  ) 3  )))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) ( + 1 1  )  ) 0  ))
(assert (not ( <= ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) 1  ) 3  )))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) ( + 1 1  )  ) 1  ) 0  ))
(assert (not ( <= ( - ( - ( - ( str.len s  ) 1  ) 1  ) ( + ( + 1 1  ) 1  )  ) 3  )))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) 1  ) ( + ( + 1 1  ) 1  )  ) 0  ))
(assert (not ( <= ( - ( - ( - ( str.len s  ) 1  ) 1  ) ( + 1 1  )  ) 3  )))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) 1  ) ( + 1 1  )  ) 0  ))
(assert (not ( <= ( - ( - ( - ( str.len s  ) 1  ) 1  ) 1  ) 3  )))
(assert ( > ( - ( - ( - ( str.len s  ) 1  ) 1  ) 1  ) 0  ))
(assert ( str.in_re s ( re.+ ( re.range "0" "9"  )  )  ))
(assert (not ( > ( str.len s  ) 12  )))
(assert (not ( = ( str.len s  ) 0  )))
(assert ( = ( str.at ( str.substr s ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  ) ( - ( str.len s  ) ( + ( + 1 ( + 1 1  )  ) ( + ( + 1 1  ) 1  )  )  )  ) 0  ) "0"  ))
(assert (str.contains generated_1 "228208082"))
(check-sat)
(exit)

commit version: bd082ab release version: 4.12.5