Soundness issue in string logic

[wintered]

(1)
11fb5c7

$ cat bug.smt2
(declare-fun a () String)
(assert (str.<= (str.replace a (str.substr a (str.indexof (str.at a 0) a 1) (+ 1 1)) a) ""))
(check-sat)
$ cvc5 -q --check-models bug.smt2
sat
$ z3 model_validate=true bug.smt2
unsat

[wintered]

(2)
found: 2025-11-18T00:21:14.747097

62cd397

$ cvc5 -q --check-models --check-proofs --strings-exp bug.smt2
sat
$ z3 model_validate=true bug.smt2
unsat
$ cat bug.smt2
(declare-fun a () Int)  
(assert (str.is_digit (str.replace (str.from_code a) 
(str.replace "a123cdef" "" (str.substr "a123cdef" (str.indexof "a123cdef"
 (str.substr "a123cdef" 0 2) a) a)) "\u0002")))  
(check-sat)  

[wintered]

(3)
ec42464

$ z3 model_validate=true bug.smt2                                               
sat                                                                             
(error "line 5 column 10: an invalid model was generated")                      
$ cat bug.smt2                                                                  
(declare-fun a () String)                                                       
(declare-fun b () String)                                                       
(assert (not (>= (ite (str.contains a "=") (+ (ite (= b "") 1 0)                
(ite (not (= (str.indexof a "=" ) (- 1))) 1 0)) 0) (str.indexof a "=" ))))      
(check-sat)                                                                     

[wingsyuyi-satori]

I have another example that appears to trigger exactly the same soundness issue. Here's a minimal version:

(declare-fun v () String)
(assert (= v (str.substr v (str.indexof v " " 1) 2)))
(check-sat)

It has the same nested substr/indexof with variable self-reference, which I believe is the key to this problem.

[wintered]

(5)

4b7e02e

$z3 model_validate=true bug.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$cat bug.smt2
(declare-fun a () String)
(assert (= (str.substr (str.++ a (str.++ a (str.from_int 0) a) 
(str.from_code (+ (str.len a) 1))) 0 (str.to_code "a")) (str.++ a "a")))
(check-sat)

[wintered]

Update 2382cd4: (5) times out on , all others still trigger

[wintered]

2382cd4

$z3 model_validate=true bug.smt2
sat
(error "line 10 column 35: an invalid model was generated")
$cat bug.smt2
(declare-fun a () String) 
(declare-const b String) 
(declare-const c String) 
(declare-fun d () Bool) 
(declare-fun e () String) 
(assert (str.in_re (str.substr a 0 (str.len (str.substr a 0 (str.len (str.from_int 0))))) 
(re.* (str.to_re (str.substr a (str.len b) (str.len e)))))) 
(assert (not (= (str.substr a 0 (str.len b)) c))) 
(assert (= d (not (= 0 (str.len (str.replace_re_all e (str.to_re "") 
(str.substr a 0 0))))))) 
(check-sat)   

[wintered]

Perhaps a little further reduced

2ea86d9

$z3 model_validate=true bug.smt2
sat
(error "line 4 column 10: an invalid model was generated")
$cat bug.smt2
(declare-fun a () String) 
(assert (str.in_re (str.from_int (str.len a)) (re.+ (str.to_re 
(str.substr a (+ (* (str.len a) (str.len a))) (str.len a)))))) 
(check-sat)            
$

[wintered]

2ea86d9

$z3 bug.smt2 
zsh: segmentation fault (core dumped)  z3 bug.smt2
$cat bug.smt2
(declare-fun r1 () Real) 
(declare-fun r2 () Real) 
(declare-fun r10 () Real) 
(assert (= r1 (/ (- (- (- 1.0 (- (- (* r2 r2 0.059 (- 1.0)))) (* r10 r2 r2)) (* r2 r2 0.059 (- 1.0)))) (- 0.0 (- 1 r1) (* (/ r1 (- 1.0)) r2 0.059 (- 1.0)))))) (assert (> (- (* (* (- 1.0 0.059) (* (- r1) (+ (- 1.0) (- 1.0 (- r1) (* r10 r2 r2)))) (/ (- (+ (- (- 0.0 (div (- 1 r1) (+ 34 (- r1) (- 1.0 (- r1) (* r10 r2 r2)))) (* r2 r2 (+ (* r10 r2 (* r1 (- 1.0))) (* r10 r2 (* r1 (- 1.0)))) (- 1.0))) r10) (- 0.0 (- 1 r1) (* r2 (+ 0.0 r10) 0.059 (- 1.0)))) 1.0) (* (- 1.0) (/ (* r10 r2 r2) (- 1.0 (- r1) (* r10 r2 (- (/ (- 1.0 (- r1) (* r10 r2 r2)) 0.0))))))) (- 1.0)) (* (- 0.0 1.0) r2 r2))) (+ (- (- 0.0 (- (mod (+ 34 (- r1) (- 1.0 (- (/ (- r1) (- 0.0 (- 1 r1) (* r2 r2 0.059 (- 1.0))))) (* r10 r2 r2))) (div (- 1 r1) (+ 34 (- (* r10 r10)) (- 1.0 (- r1) (- r10))))) (- (- (* 1.0 0.059)))) (* (- 0.0) r2 0.059 (- (- r2)))) r1) (- (/ (* r2 (/ (- 1.0 (- r1) (* r10 r2 r2)) 0.0) (- r1) (- (- 0.0 (- 1 (* r1 (to_real (- 1 r1)))) (- (- (- 1.0 (- r1))) (to_real 1))))) (- (- (* r2 0.0)) (- 1 (- r2 (* r2 r2 0.059 (- 1.0)))) (- (- 1.0 (- r1) (* r10 r2 r2)) r10))))))) 
(check-sat)       
$