From 9bde93f81286fd71565d74a80556b907527bf4b3 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <mtrberzi@users.noreply.github.com>
Date: Tue, 23 Feb 2021 10:36:14 -0600
Subject: [PATCH] z3str3: check whether rewritten axioms rewrite to TRUE
 (#5039)

---
 src/smt/theory_str.cpp | 1 +
 1 file changed, 1 insertion(+)

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);
     }