relax unhandled condition

Z3Prover · Nov 14, 2020 · 98db260 · 98db260
1 parent 49a0266
commit 98db260
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
@@ -323,7 +323,8 @@ namespace smt {
                 literal is_nullable_lit = th.mk_literal(is_nullable);
                 ctx.mark_as_relevant(is_nullable_lit);
                 th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
-                th.add_unhandled_expr(is_nullable);
+                if (str().is_in_re(is_nullable))
+                    th.add_unhandled_expr(is_nullable);
             }
         }