invalid model issue on an incremental string formula

[zhendongsu]

[659] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
(error "line 27 column 10: an invalid model was generated")
(
  (define-fun a () Int
    1)
  (define-fun b () Bool
    true)
  (define-fun s () String
    "220044AB")
)
[660] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Bool)
(declare-fun s () String)
(push)
(check-sat)
(assert (> (- (str.len s) 2 2 (+ 1 1 1)) 0))
(check-sat)
(assert (= "0" (str.at (str.substr s 2 2) 0)))
(check-sat)
(assert (not (= 1 (str.len (str.substr s 2 2)))))
(check-sat)
(assert (< (ite (str.prefixof "-" (str.substr s 0 (- 1 0))) (str.to_int (str.substr s 0 (+ 1 1))) 0) 255))
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(push)
(assert (> (str.len s) 0))
(check-sat)
(push)
(assert b)
(assert (> a 0))
(check-sat)
(assert (not (<= (ite (str.prefixof "-" (str.substr s 2 (- (+ 1 1 1 (- 1 1)) 1))) (- (str.to_int (str.substr (str.substr s 3 (- 3 1)) 1 (- (str.len (str.substr s 3 (+ 1 1 1 1 1))) 1)))) (str.to_int (str.substr s 3 (- (+ 1 1 1 1 1 1) 3)))) 255)))
(check-sat)
(check-sat)
(get-model)

[zhendongsu]

Another very similar instance:

[521] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
(error "line 16 column 10: an invalid model was generated")
(
  (define-fun c () Bool
    false)
  (define-fun a () Bool
    true)
  (define-fun b () Int
    (- 2))
  (define-fun s () String
    "BCDEF400")
)
[522] % cat small.smt2
(declare-const a Bool)
(declare-const b Int)
(declare-const c Bool)
(declare-fun s () String)
(assert (not (= "0" (str.at (str.substr s 0 (+ 1 b)) 0))))
(assert a)
(assert (> (- (str.len s) 3) 3))
(assert (> (- (str.len s) 5) 0))
(check-sat)
(check-sat)
(assert (not (= 1 (str.len (str.substr s 2 (- (str.len s) 6))))))
(check-sat)
(push)
(assert (= (ite c (- (str.to_int (str.substr (str.substr s 5 2) 1 (- (str.len (str.substr s 5 3)) 1)))) (str.to_int (str.substr s 5 5))) 255))
(check-sat)
(check-sat)
(get-model)

[zhendongsu]

Invalid model on a non-incremental instance:

[547] % z3release model_validate=true small.smt2 
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun x () String
    "4003")
  (define-fun a () Int
    1)
)
[548] % cat small.smt2 
(declare-fun a () Int)
(declare-fun x () String)
(assert (= 0 (* (str.len (str.at x 1)) (ite (= 0 (* a (+ 1 (str.len (str.at x 0))))) 0 a) (ite (ite (= 0 a) true (= (str.to_int x) (+ (* a a a) (* a a a) (* a a a)))) 0 1))))
(assert (< 0 a))
(assert (< (+ a a) (str.len x)))
(check-sat)
(get-model)

[zhendongsu]

Another instance:

[608] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
(error "line 23 column 10: an invalid model was generated")
(
  (define-fun a () Int
    49)
  (define-fun d () Int
    5)
  (define-fun b () Bool
    true)
  (define-fun c () Bool
    true)
  (define-fun x208__fresh () Int
    (- 32286))
  (define-fun s () String
    "A004BCD")
)
[609] % cat small.smt2
(declare-const a Int)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Int)
(declare-const x208__fresh Int)
(declare-fun s () String)
(push)
(assert (<= (str.len s) 9))
(check-sat)
(push)
(assert (> (str.len s) 6))
(check-sat)
(assert b)
(check-sat)
(assert c)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(assert (not (<= (ite (str.prefixof "-" (str.substr s 1 x208__fresh)) (str.to_int (str.substr (str.substr s 1 3) 1 (- (str.len (str.substr s 1 (- 4 1))) 1))) (str.to_int (str.substr s 1 3))) 255)))
(check-sat)
(assert (ite (str.prefixof "-" (str.substr s 1 d)) true (ite (= a (- 1)) false true)))
(check-sat)
(get-model)

[wintered]

$z3release model_validate=true bug.smt2                                            
sat                                                                                
(error "line 5 column 10: an invalid model was generated")                         
$cat bug.smt2                                                                      
(declare-fun T_2 () Bool)                                                          
(declare-fun var_0xINPUT_540541 () String)                                         
(assert (= T_2 (= 1 (str.len var_0xINPUT_540541))))                                
(assert (not (<= (ite (str.prefixof "-" (str.substr var_0xINPUT_540541 (+ 1 1) (- (+ 1 1 1 1 1) 
(+ 1 1)))) (- (str.to_int (str.substr (str.substr var_0xINPUT_540541 (+ 1 1) (- (+ 1 1 1 1 1) (+ 1 1))) 1 
(- (str.len (str.substr var_0xINPUT_540541 (+ 1 1) (- (+ 1 1 1 1 1) (+ 1 1)))) 1)))) (str.to_int 
(str.substr var_0xINPUT_540541 (+ 1 1) (- (+ 1 1 1 1 1) (+ 1 1))))) 255)))
(check-sat)%                                                                        
$  

[zhendongsu]

Another instance:

[605] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
(error "line 14 column 10: an invalid model was generated")
[606] % cat small.smt2
(declare-const a Bool)
(declare-const b Int)
(declare-const s String)
(declare-const x Int)
(declare-const y Bool)
(check-sat)
(assert (> (str.len s) 10))
(check-sat)
(assert (> (str.len s) 0))
(check-sat)
(assert (not (<= (ite (str.prefixof "-" (str.substr s 0 (+ 1 1 1))) (- (str.to_int (str.substr (str.substr s 0 (+ 1 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1 1))) 1)))) (str.to_int (str.substr s 0 (+ 1 (+ 1 1))))) 255)))
(check-sat)
(assert (ite a (= x (str.to_int (str.substr s 0 b))) y))
(check-sat)

[zhendongsu]

[539] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
[540] % z3release model_validate=true smt.threads=2 small.smt2
sat
sat
sat
sat
sat
(error "line 10 column 10: an invalid model was generated")
[541] % cat small.smt2
(declare-fun a () Bool)
(declare-fun s () String)
(check-sat)
(assert (= 1 (str.len (str.substr s 0 1))))
(check-sat)
(assert (> (- (str.len s) 1 1 (+ 1 1 1)) (<= (ite (str.prefixof "-" (str.substr s 1 (+ 1 1 1))) (- (str.to_int (str.substr (str.substr s 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)))) 255)))
(check-sat)
(assert a)
(check-sat)
(check-sat)

[zhendongsu]

A solution unsoundness instance:

[515] % z3release small.smt2
sat
sat
sat
sat
sat
unsat
unsat
unsat
[516] % z3release smt.threads=2 small.smt2
sat
sat
sat
sat
sat
unsat
unsat
sat
[517] % cat small.smt2
(declare-fun s () String)
(check-sat)
(assert (not (= (str.len (str.substr s 1 (- (+ 1 (+ 1 1)) 1))) 1)))
(check-sat)
(assert (= (str.len (str.substr s 0 (- 1 0))) 1))
(check-sat)
(assert (<= (- (- (- (str.len s) 1) (+ 1 1)) 0) 3))
(check-sat)
(assert (> (- (- (- (str.len s) 1) (+ 1 1)) (+ 1 1)) 0))
(check-sat)
(assert (not (<= (ite (str.contains "-" (str.substr s (+ 0 ) (-
  (str.len s) (- (+ 1 (+ 1 1)) 1)))) (- (str.to_int (str.substr
  (str.substr s (+ (+ 1 (+ 1 1)) 1) (- (str.len s) 1 )) 1 (- (str.len
  (str.substr s (+ (+ 1 (+ 1 1)) 1) (- (str.len s) (+ (+ 1 1 ) 1))))
  1)))) (str.to_int (str.substr s (+ (+ 1 (+ 1 1)) 1) (- (str.len s)
  (+ (+ 1 1 ) 1))))) 255)))
(check-sat (ite (str.prefixof "" (str.substr s 0 (- 0))) (or (ite (= 0
  (str.to_int (str.substr (str.substr s 0 (- (+ 0))) 1 (- (str.len
  (str.substr s (* 1 ) 0)) 1)))) false true) (> 0 1)) (ite (distinct
  (- 1) (str.to_int (str.substr s (+ (- (+ 1))) (- (- (+ 1 (+ 1
  1))))))) false true)))
(check-sat)
(check-sat)

[depted]

An instance that causes invalid model bug

commit: 304b316

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

$ cat ./small.smt2
(declare-fun v () String)
(declare-fun m () Int)
(assert (< 0 (- (- (seq.last_indexof "JH" v)) m)))
(check-sat)

[zhendongsu]

Nikolaj (@NikolajBjorner), looks like the following two instances still reproduce:

• https://github.com/Z3Prover/z3/issues/6346#issuecomment-1250763728
• https://github.com/Z3Prover/z3/issues/6346#issuecomment-1256913930

[zhendongsu]

[604] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
(error "line 46 column 10: an invalid model was generated")
[605] % cat small.smt2
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-fun s () String)
(push)
(assert (not (= (str.len (str.substr s (+ (+ 1 1) 1) (- (+ (+ (+ 1 1) 1) (+ 1 1)) (+ (+ 1 1) 1)))) 1)))
(check-sat)
(push)
(assert (<= (ite (str.prefixof "-" (str.substr s 0 (- (+ (+ 1 1) 1) 0))) (- (str.to_int (str.substr (str.substr s 0 (- (+ (+ 1 1) 1) 0)) 1 (- (str.len (str.substr s 0 (- (+ (+ 1 1) 1) 0))) 1)))) (str.to_int (str.substr s 0 (+ 0 1)))) 255))
(check-sat)
(push)
(assert (ite (str.prefixof "-" (str.substr s 0 (- (+ (+ 1 1) 1) 0))) (and (ite (= 1 (str.to_int (str.substr (str.substr s 0 (- (+ (+ 1 1) 1) 0)) 1 (- (str.len (str.substr s 0 (- (+ (+ 1 1) 1) 0))) 1)))) false true) (> (str.len (str.substr s 0 (- (+ (+ 1 1) 1) 0))) 1)) (ite (= (- 1) (str.to_int (str.substr s 0 (- (+ (+ 1 1) 1) 0)))) false true)))
(check-sat)
(push)
(assert (not (= (str.at (str.substr s 0 (- (+ (+ 1 1) 1) 0)) 0) "0")))
(check-sat)
(push)
(assert (not (= (str.len (str.substr s 0 (- (+ (+ 1 1) 1) 0))) 1)))
(check-sat)
(push)
(assert (<= 1 3))
(check-sat)
(push)
(check-sat)
(check-sat)
(check-sat)
(push)
(assert (> (- (str.len s) 1) 0))
(check-sat)
(push)
(assert (not (<= (- (str.len s) (+ c 1)) 3)))
(check-sat)
(push)
(assert (> (- (- (str.len s) 1) (+ (+ 1 1) 1)) 0))
(check-sat)
(push)
(assert (not (<= (- (- (str.len s) (+ 1 1)) 1) 0)))
(check-sat)
(check-sat)
(check-sat)
(push)
(assert (> (- (- (- (str.len s) 0) 1) 1) 0))
(check-sat)
(push)
(assert (not (distinct (ite (str.prefixof "-" (str.substr s (mod (+ 1 1) (+ (+ 1 1) 1)) a)) (- (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 b (- (+ (+ (+ 1 1) (+ (+ 1 1) 1)) (+ (+ 1 1) 1)) (+ (+ 1 1) (+ (+ 1 1) 1))))) 1)))) (str.to_int (str.substr s (+ (+ 1 1) 0) (- (+ a a) a)))) 255)))
(check-sat)

[zhendongsu]

[522] % z3release model_validate=true small.smt2
sat
sat
sat
sat
(error "line 10 column 10: an invalid model was generated")
[523] % cat small.smt2
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun s () String)
(check-sat)
(assert (> (str.len s) 8))
(check-sat)
(assert (not (<= (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (- (str.to_int (str.substr (str.substr s 2 3) 1 (- (str.len (str.substr s (+ 1 1) 3)) 1)))) (str.to_int (str.substr s 2 3))) 255)))
(check-sat)
(assert (ite x (ite y false true) true))
(check-sat)