diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 5aef06531..99e91f85e 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -518,6 +518,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         st = mk_str_in_regexp(args[0], args[1], result);
         break;
+    case OP_STRING_LE:
+        SASSERT(num_args == 2);
+        st = mk_str_le(args[0], args[1], result);
+        break;
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_STRING_ITOS: 
@@ -1237,6 +1241,11 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_str_le(expr* a, expr* b, expr_ref& result) {
+    result = m.mk_not(m_util.str.mk_lex_lt(b, a));
+    return BR_DONE;
+}
+
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;
     if (m_autil.is_numeral(a, r)) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index acc494b09..0cfb8639e 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -124,6 +124,7 @@ class seq_rewriter {
     br_status mk_str_stoi(expr* a, expr_ref& result);
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
     br_status mk_str_to_regexp(expr* a, expr_ref& result);
+    br_status mk_str_le(expr* a, expr* b, expr_ref& result);
     br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_re_union(expr* a, expr* b, expr_ref& result);
     br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index efd074f69..5852992da 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -5923,6 +5923,9 @@ void theory_seq::propagate_not_suffix(expr* e) {
    e1 < e2 => e1 = empty or e1 = xcy
    e1 < e2 => e1 = empty or c < d
    e1 < e2 => e2 = xdz
+   !(e1 < e2) => e1 = e2 or e2 = empty or e2 = xcy
+   !(e1 < e2) => e1 = e2 or e2 = empty or c < d
+   !(e1 < e2) => e1 = e2 or e1 = xdz
    
    e1 < e2 or e1 = e2 or e2 < e1
    !(e1 = e2) or !(e1 < e2)
@@ -5941,15 +5944,23 @@ void theory_seq::add_lt_axiom(expr* n) {
     expr_ref z = mk_skolem(symbol("str.lt.z"), e1, e2);
     expr_ref c = mk_skolem(symbol("str.lt.c"), e1, e2, nullptr, nullptr, char_sort);
     expr_ref d = mk_skolem(symbol("str.lt.d"), e1, e2, nullptr, nullptr, char_sort);
+    expr_ref xcy(mk_concat(x, m_util.str.mk_unit(c), y), m);
+    expr_ref xdz(mk_concat(x, m_util.str.mk_unit(d), z), m);
     expr_ref empty_string(m_util.str.mk_empty(s), m);
     literal emp1 = mk_eq(e1, empty_string, false);
+    literal emp2 = mk_eq(e2, empty_string, false);
     literal eq   = mk_eq(e1, e2, false);
-    literal xcy  = mk_eq(e1, mk_concat(x, m_util.str.mk_unit(c), y), false);
-    literal xdz  = mk_eq(e2, mk_concat(x, m_util.str.mk_unit(d), z), false);
+    literal e1xcy = mk_eq(e1, xcy, false);
+    literal e2xdz = mk_eq(e2, xdz, false);
+    literal e2xcy = mk_eq(e2, xcy, false);
+    literal e1xdz = mk_eq(e1, xdz, false);
     literal ltcd = mk_literal(m_util.mk_lt(c, d));
-    add_axiom(~lt, xdz);
-    add_axiom(~lt, emp1, xcy);
+    add_axiom(~lt, e2xdz);
+    add_axiom(~lt, emp1, e1xcy);
     add_axiom(~lt, emp1, ltcd);
+    add_axiom(lt, eq, e1xdz);
+    add_axiom(lt, eq, emp2, ltcd);
+    add_axiom(lt, eq, emp2, e2xcy);
     if (e1->get_id() <= e2->get_id()) {
         literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1));
         add_axiom(lt, eq, gt);