From e8690d28f819244797ed6584599ee3be171d58fc Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 3 Jul 2020 17:13:27 -0500 Subject: [PATCH] z3str3: continue instead of incorrectly giving up in solve_regex_automata (#4556) --- src/smt/theory_str_regex.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 9cc96f21c..da96b13bb 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -203,7 +203,7 @@ namespace smt { continue; } else { // fixed-length model construction handles path constraints on our behalf, and with a better reduction - return false; + continue; } } else { // no automata available, or else all bounds assumptions are invalid