(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (distinct (str.++ a b) (str.++ b a) c))
(assert (distinct a c))
(check-sat)

(smt.diff_logic: non-diff logic expression (let ((a!1 (* (- 1) (+ 1 (str.len (seq.tail c 0))))))
  (+ (str.len c) a!1)))
(smt.diff_logic: non-diff logic expression (let ((a!1 (* (- 1) (+ 1 (str.len (seq.tail a 0))))))
  (+ (str.len a) a!1)))
ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 976
parent->is_cgr()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB