text: ; 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)
  