From 11d5b508be5c7e2ee3d81fcd656f9784b9119d35 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Aug 2020 10:14:39 -0700 Subject: [PATCH] fix #4625 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str_regex.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 1b376dfbf3b..fdad98b46ed 100644 --- 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 {