diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 8fabe8163..58a3cb34c 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -139,10 +139,12 @@ namespace seq {
             extract_prefix_axiom(e, s, l);
             return;
         }
+#if 0
         if (is_extract_suffix(s, _i, _l)) {
-            extract_suffix_axiom(e, i, l);
+            extract_suffix_axiom(e, s, i);
             return;
         }
+#endif
         TRACE("seq", tout << s << " " << i << " " << l << "\n";);
         expr_ref x = m_sk.mk_pre(s, i);
         expr_ref ls = mk_len(_s);
diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index df21a0c5a..940d81fe0 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -128,6 +128,10 @@ void seq_axioms::add_extract_axiom(expr* e) {
         add_extract_prefix_axiom(e, s, l);
         return;
     }
+    if (is_extract_suffix(s, i, l)) {
+        add_extract_suffix_axiom(e, s, i);
+        return;
+    }
     expr_ref x = m_sk.mk_pre(s, i);
     expr_ref ls = mk_len(s);
     expr_ref lx = mk_len(x);
@@ -213,6 +217,12 @@ bool seq_axioms::is_extract_prefix0(expr* s, expr* i, expr* l) {
     return a.is_numeral(i, i1) && i1.is_zero();    
 }
 
+bool seq_axioms::is_extract_suffix(expr* s, expr* i, expr* l) {
+    expr_ref len(a.mk_add(l, i), m);
+    m_rewrite(len);
+    return seq.str.is_length(len, l) && l == s;
+}
+
 
 /*
   s = ey
@@ -235,6 +245,28 @@ void seq_axioms::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
 }
 
 
+/*
+  s = xe
+  0 <= i <= len(s) => i = len(x)    
+  i < 0 => e = empty
+  i > len(s) => e = empty
+*/
+void seq_axioms::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
+    TRACE("seq", tout << "suffix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << "\n";);
+    expr_ref x = m_sk.mk_pre(s, i);
+    expr_ref lx = mk_len(x);
+    expr_ref ls = mk_len(s);
+    expr_ref xe = mk_concat(x, e);
+    literal emp = mk_eq_empty(e);
+    literal i_ge_0 = mk_ge(i, 0);
+    literal i_le_s = mk_le(mk_sub(i, ls), 0);
+    add_axiom(mk_eq(s, xe));
+    add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx));
+    add_axiom(i_ge_0, emp);
+    add_axiom(i_le_s, emp);
+}        
+
+
 /*
   encode that s is not contained in of xs1
   where s1 is all of s, except the last element.
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index f3a443497..d986fccf1 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -60,7 +60,9 @@ namespace smt {
         bool is_drop_last(expr* s, expr* i, expr* l);
         bool is_tail(expr* s, expr* i, expr* l);
         bool is_extract_prefix0(expr* s, expr* i, expr* l);
+        bool is_extract_suffix(expr* s, expr* i, expr* l);
         void add_extract_prefix_axiom(expr* e, expr* s, expr* l);
+        void add_extract_suffix_axiom(expr* e, expr* s, expr* i);
         void tightest_prefix(expr* s, expr* x);
         void ensure_digit_axiom();
         void add_clause(expr_ref_vector const& lits);