approximate min-length for complements

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 19, 2020 · ed258ca · ed258ca
1 parent 4857d60
commit ed258ca
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
@@ -1668,8 +1668,7 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
         case OP_RE_PLUS:
             return get_info_rec(e->get_arg(0));
         case OP_RE_COMPLEMENT:
-            i1 = get_info_rec(e->get_arg(0));
-            return info(i1.min_length > 0 ? 0 : UINT_MAX);
+            return info(0); 
         case OP_RE_LOOP:
             i1 = get_info_rec(e->get_arg(0));
             return info(u.max_mul(i1.min_length, e->get_decl()->get_parameter(0).get_int()));
@@ -1687,4 +1686,4 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
         return info(std::min(i1.min_length, i2.min_length));
     }
     return invalid_info;
-}
+}