From 0146259ea402a8bf3996f1ca0d2d37ed69fddd35 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 12 Feb 2020 13:46:27 -0500
Subject: [PATCH] z3str3: fix control flow and return paths in regex model
 construction

---
 src/smt/theory_str_mc.cpp | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index d3e31e675..aa3e215b7 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -488,6 +488,9 @@ namespace smt {
                 cex = m.mk_or(f, m.mk_not(ctx.mk_eq_atom(mk_strlen(str), mk_int(0))));
                 ctx.get_rewriter()(cex);
                 return false;
+            } else {
+                TRACE("str_fl", tout << "regex constraint satisfied without asserting constraints to subsolver" << std::endl;);
+                return true;
             }
         } else {
             expr_ref_vector trail(m);
@@ -560,6 +563,9 @@ namespace smt {
                     cex = m.mk_or(m.mk_not(f), m.mk_not(ctx.mk_eq_atom(mk_strlen(str), mk_int(str_chars.size()))));
                     ctx.get_rewriter()(cex);
                     return false;
+                } else {
+                    TRACE("str_fl", tout << "regex constraint satisfied without asserting constraints to subsolver" << std::endl;);
+                    return true;
                 }
             } else {
                 // TODO fixed_length_lesson?
@@ -571,8 +577,6 @@ namespace smt {
                 return true;
             }
         }
-        UNREACHABLE(); // added because compiler complains that not all control paths return a value.
-        return false;
     }
 
     /*