From 524434cfbb70eb25e96a8013e4548b347f20a16d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 9 Feb 2020 12:52:57 -0500
Subject: [PATCH] z3str3: pass correct subterm to negative regex model
 construction

---
 src/smt/theory_str_mc.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index cdb511777..b59f937e0 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -906,7 +906,7 @@ namespace smt {
                     } else if (u.str.is_in_re(subterm)) {
                         TRACE("str_fl", tout << "reduce negative regex membership: " << mk_pp(f, m) << std::endl;);
                         expr_ref cex_clause(m);
-                        expr_ref re(f, m);
+                        expr_ref re(subterm, m);
                         if (!fixed_length_reduce_regex_membership(subsolver, re, cex_clause, false)) {
                             assert_axiom(cex_clause);
                             add_persisted_axiom(cex_clause);