Unsoundness issue with smt.string_solver=z3str3

[nicdard]

Hi,

for the following formula z3 incorrectly reports sat instead of unsat.

$ cat test.smt2
(declare-fun s () String)
(declare-fun r () String)
(assert 
  (and 
    (= 
      "\u{2f}" (str.substr s 0 (str.len "lo"))) 
      (str.in_re r (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\") (re.* re.allchar)))
    ) 
    (= 
      (str.substr r 0 (str.len (str.++ r ""))) (str.++ (str.++ (str.substr s 0 (str.len "lo")) s) 
      (str.substr s 0 1))
    )
  )
)
(check-sat)

$ z3 smt.string_solver=z3str3 test.smt2 
sat

$ z3 --version
Z3 version 4.9.2 - 64 bit

OS: Ubuntu 20.04

[NikolajBjorner]

There is currently a stream of bugs reported to z3str3 but at this point no reaction on when or whether they are going to be addressed. If there is no response, it will be more practical to lump these bugs into a larger issue. In the past we ended up with a large fraction of open issues against z3 being for z3str3.

[nicdard]

Ok, then I will add more issue to this thread if I find more regarding z3str3

[zhendongsu]

Adding a few cases (there seem to be quite many):

[514] % z3release small.smt2 
unsat
[515] % z3release smt.string_solver=z3str3 small.smt2 
sat
[516] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
sat
(error "line 3 column 10: an invalid model was generated")
[517] % cat small.smt2 
(declare-fun a () String)
(assert (not (str.<= a a)))
(check-sat)

[zhendongsu]

[522] % z3release small.smt2 
unsat
[523] % z3release smt.string_solver=z3str3 small.smt2 
sat
[524] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
sat
(error "line 3 column 10: an invalid model was generated")
[525] % cat small.smt2 
(declare-fun x () String)
(assert (not (= (str.contains x (str.++ x x x)) (= x ""))))
(check-sat)

[zhendongsu]

[533] % z3release model_validate=true small.smt2 
sat
[534] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
sat
(error "line 3 column 10: an invalid model was generated")
[535] % cat small.smt2
(declare-fun a () String)
(assert (str.suffixof a (str.from_code (str.indexof a "A" 0))))
(check-sat)

[zhendongsu]

[539] % z3release model_validate=true small.smt2 
unsat
[540] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
sat
(error "line 3 column 10: an invalid model was generated")
[541] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re "AB" (re.union (str.to_re "A") (str.to_re (ite (str.in_re a (re.* (str.to_re "B"))) a "")))))
(check-sat)

[zhendongsu]

[545] % z3release model_validate=true small.smt2 
sat
[546] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
unsat
[547] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.from_int (str.len a)) (re.union (str.to_re "0") (str.to_re "A"))))
(check-sat)

[zhendongsu]

[558] % z3release model_validate=true small.smt2 
sat
[559] % z3release smt.string_solver=z3str3 small.smt2 
unsat
[560] % cat small.smt2 
(declare-fun x () String)
(declare-fun y () String)
(assert (distinct (ite (= "" (str.replace x (str.++ y y) (str.replace (str.++ "9" (str.++ x y) y) x (str.replace y y y)))) (str.replace x y y) y) y (str.++ (str.replace y (str.++ x y) y) (str.++ (str.++ y y) (str.replace y y y)))))
(check-sat)

[zhendongsu]

[568] % z3release model_validate=true small.smt2 
sat
[569] % z3release smt.string_solver=z3str3 small.smt2 
unsat
[570] % cat small.smt2 
(declare-fun v () String)
(assert (>= (str.len (str.substr v 2 1)) 1))
(assert (>= 0 (str.indexof (str.substr v 0 (- (str.len v) 1)) "N" 1)))
(assert (str.contains (str.substr v 0 (- (str.len v) 1)) "N"))
(check-sat)

[zhendongsu]

[574] % z3release model_validate=true small.smt2 
sat
[575] % z3release smt.string_solver=z3str3 small.smt2 
unsat
[576] % cat small.smt2 
(declare-const x Int)
(declare-fun v () String)
(assert (>= 0 (str.indexof (str.substr v 0 (- (str.len v) 1)) "N" 1)))
(assert (str.contains (str.substr v 0 (- (str.len v) 1)) "N"))
(assert (str.contains (str.substr (str.substr v 0 x) 1 (- (str.len (str.substr v 0 (- (str.len v) 1))) 1)) "O"))
(check-sat)

[JohnLyu2]

[522] % z3release small.smt2 
unsat
[523] % z3release smt.string_solver=z3str3 small.smt2 
sat
[524] % z3release smt.string_solver=z3str3 model_validate=true small.smt2 
sat
(error "line 3 column 10: an invalid model was generated")
[525] % cat small.smt2 
(declare-fun x () String)
(assert (not (= (str.contains x (str.++ x x x)) (= x ""))))
(check-sat)

This bug has been fixed in #6312