diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index edc91e21f..6458e36af 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1043,12 +1043,19 @@ namespace seq {
     }
 
     /**
+       suffix(s, t):
+       - the sequence s is a suffix of t.
 
-       suffix(s, t) => s = seq.suffix_inv(s, t) + t
+       Positive case is handled by the solver when the atom is asserted
+       suffix(s, t) => t = seq.suffix_inv(s, t) + s
+
+       Negative case is handled by axioms when the negation of the atom is asserted
        ~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t)
        ~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t)
        ~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t)
 
+       Symmetric axioms are provided for prefix
+
     */
 
     void axioms::suffix_axiom(expr* e) {