Soundness issue in string logic

[wintered]

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]

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)