fix #4625

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 12, 2020 · 11d5b50 · 11d5b50
1 parent 4045563
commit 11d5b50
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
@@ -844,8 +844,6 @@ namespace smt {
             return false;
         } else if (u.re.is_intersection(re)) {
             return false;
-        } else if (u.re.is_complement(re)) {
-            return false;
         } else if (u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
             return check_regex_length_linearity_helper(sub1, already_star);
         } else {