diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index e0dfa4384..270030d45 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -237,6 +237,7 @@ namespace smt {
         ast_manager & m = get_manager();
         expr_ref _e(e, m);
         ctx.get_rewriter()(_e);
+        if (m.is_true(_e)) return;
         assert_axiom(_e);
     }