[541] % z3 small.smt2
(smt.diff_logic: non-diff logic expression (+ y (str.indexof (seq.idx.right (seq.unit #x42) x y) x 0)))
unknown
[542] % z3 smt.string_solver=z3str3 small.smt2
(smt.diff_logic: non-diff logic expression (+ (str.len t0!tmp2) (str.len t1!tmp3)))
ASSERTION VIOLATION
File: ../src/smt/arith_eq_adapter.cpp
Line: 84
n1 != n2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[543] % 
[543] % cat small.smt2
(set-option :smt.arith.solver 1)
(declare-fun x () String)
(declare-fun y () Int)
(assert (distinct (str.substr x 1 (str.indexof "B" x y)) ""))
(check-sat)
[544] %