diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 490c9daf3..f8cb8586e 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -459,7 +459,8 @@ bool theory_seq::branch_binary_variable(depeq const& e) {
     }
     if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
         // |x| - |y| = |ys| - |xs|
-        expr_ref a(mk_sub(mk_len(x), mk_len(y)), m);
+        auto p0 = mk_len(x);
+        expr_ref a(mk_sub(p0, mk_len(y)), m);
         expr_ref b(m_autil.mk_int(rational(ys.size())-rational(xs.size())), m);
         propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
         return true;
@@ -702,7 +703,8 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
     
     literal_vector lits;
     if (xs == ys) {
-        literal lit = mk_eq(mk_len(x1), mk_len(y1), false);
+        auto p0 = mk_len(x1);
+        literal lit = mk_eq(p0, mk_len(y1), false);
         if (ctx.get_assignment(lit) == l_undef) {
             TRACE(seq, tout << mk_pp(x1, m) << " = " << mk_pp(y1, m) << "?\n";);
             ctx.mark_as_relevant(lit);
@@ -1007,7 +1009,8 @@ bool theory_seq::propagate_length_coherence(expr* e) {
         // len(e) <= hi => len(tail) <= hi - lo
         expr_ref high1(m_autil.mk_le(len_e, m_autil.mk_numeral(hi, true)), m);
         if (hi == lo) {
-            add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
+            auto p0 = ~mk_literal(high1);
+            add_axiom(p0, mk_seq_eq(seq, emp));
             added = true;
         }
         else {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 88e5b3ce5..21e1944f8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1587,7 +1587,8 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
     m_trail_stack.push(insert_obj_map<expr, unsigned>(m_length_limit_map, s));
     if (is_searching) {
         expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
-        add_axiom(~mk_literal(dlimit), mk_literal(lim_e));
+        auto p0 = ~mk_literal(dlimit);
+        add_axiom(p0, mk_literal(lim_e));
     }
 }
 
@@ -3062,7 +3063,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_sk.mk_prefix_inv(se1, se2);
             f = mk_concat(se1, f);
             propagate_eq(lit, f, se2, true);
-            propagate_eq(lit, mk_len(f), mk_len(se2), false);
+            auto p0 = mk_len(f);
+            propagate_eq(lit, p0, mk_len(se2), false);
         }
         else {
             propagate_not_prefix(e);
diff --git a/sus.py b/sus.py
index 4db234483..66f2baf72 100644
--- a/sus.py
+++ b/sus.py
@@ -5,6 +5,8 @@ and print matches in grep-like format: file:line:match
 """
 import os
 import re
+# skip chain calls like obj.method(...)
+chain_pattern = re.compile(r"\.\s*[A-Za-z_]\w*\s*\(")
 
 # pattern: identifier(... foo(...), ... bar(...)) with two function-call args
 pattern = re.compile(
@@ -28,7 +30,10 @@ for root, dirs, files in os.walk('src/smt'):
                 for i, line in enumerate(f, 1):
                     if pattern.search(line):
                         # skip lines with TRACE or ASSERT in all caps
-                        if any(word in line for word in excl):
+                        if 'TRACE' in line or 'ASSERT' in line or 'VERIFY' in line:
+                            continue
+                        # skip chain calls (method-style chaining)
+                        if chain_pattern.search(line):
                             continue
                         full_path = os.path.abspath(path)
                         print(f"{full_path}:{i}:{line.rstrip()}")