Commit: d5c6abe
$ z3-4.8.10 unknown.smt2
sat
$ z3 unknown.smt2
unknown
$ cat unknown.smt2
(declare-const x Int)
(declare-fun T () Int)
(declare-fun va () String)
(assert (distinct (str.from_int T) (str.replace va (str.replace "" va "") (str.from_int (- x)))))
(check-sat)
Manually applying the rewrite (str.replace "" va "") = "" results in the formula being decidable:
$ z3-4.8.10 known.smt2
sat
$ z3 known.smt2
sat
$ cat known.smt2
(declare-const x Int)
(declare-fun T () Int)
(declare-fun va () String)
(assert (distinct (str.from_int T) (str.replace va "" (str.from_int (- x)))))
(check-sat)
Commit: d5c6abe
Manually applying the rewrite
(str.replace "" va "") = ""results in the formula being decidable: