From 812049ca4a5306fe0c444110f51802ff215d30b1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 20 Jan 2020 19:43:40 -0500
Subject: [PATCH] z3str3: ignore non-relevant formulas in bitvector model
 construction

---
 src/smt/theory_str_mc.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index 3099a29c0..d0bc6bc20 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -659,6 +659,10 @@ namespace smt {
         sort * bool_sort = m.mk_bool_sort();
 
         for (expr * f : formulas) {
+            if (!get_context().is_relevant(f)) {
+                TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;);
+                continue;
+            }
             // reduce string formulas only. ignore others
             sort * fSort = m.get_sort(f);
             if (fSort == bool_sort && !is_quantifier(f)) {