; EXPECT: sat
(set-logic QF_S)
(declare-fun _substvar_270_ () String)
(declare-fun _substvar_273_ () Bool)
(declare-fun _substvar_275_ () Bool)
(declare-fun _substvar_293_ () Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const Str3 String)
(declare-const Str7 String)
(declare-const Str15 String)
(assert (or (xor true true (xor v0 v3 false v1 false v2 v2 v1 false v2 v1) true true (=> (or v1 (distinct Str15 _substvar_270_ Str3 (str.++ Str7 Str7)) v2) false) false true) _substvar_275_))
(check-sat)