Hello,

Z3 abd1674 returns unknown for the following formula. However, the term like (str.<= "" s) within it could be directly simplified to true.

Here’s a minimal example:

$ z3 small.smt2 
unknown
$ cat small.smt2 
(declare-fun v () String)
(assert (str.<= "" (str.replace_all v "i" v)))
(check-sat)

Thank you for your attention!