1 2 3 4 5 6 7 8 9 10 11 12 13
(set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status sat) (set-option :strings-exp true) (set-option :strings-fmf true) (set-option :produce-models true) (declare-fun x () String) (declare-fun y () String) (declare-fun z () String) (assert (not (= x ""))) (assert (not (= y ""))) (assert (not (= (str.replace x y z) (str.replace_all x y z)))) (check-sat)