get_len_expr: fixing asserts during quantifier handling

VeriFIT · Jan 2, 2025 · fd03518 · fd03518
1 parent b6435e5
commit fd03518
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -140,7 +140,11 @@ namespace smt::noodler {
         for (unsigned i = 0; i < nFormulas; ++i) {
             STRACE("str-init-formula", tout << "Initial asserted formula " << i << ": " << expr_ref(ctx.get_asserted_formula(i), m) << std::endl;);
             obj_hashtable<app> lens;
-            util::get_len_exprs(to_app(ctx.get_asserted_formula(i)), m_util_s, m, lens);
+            // it seems Z3 is asserting formulae under quantification separately; 
+            // we can skip quantified formulae as the lenght variables were computed before.
+            if(!is_quantifier(ctx.get_asserted_formula(i))) {
+                util::get_len_exprs(to_app(ctx.get_asserted_formula(i)), m_util_s, m, lens);
+            }
             for (app* const a : lens) {
                 util::get_str_variables(a, this->m_util_s, m, this->len_vars, &this->predicate_replace);
             }

diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc
@@ -125,6 +125,11 @@ namespace smt::noodler::util {
         }
 
         for(unsigned i = 0; i < ex->get_num_args(); i++) {
+            // it seems Z3 is asserting formulae under quantification separately; 
+            // we can skip quantified formulae as the lenght variables were computed before.
+            if(is_quantifier(ex->get_arg(i))) {
+                return;
+            }
             SASSERT(is_app(ex->get_arg(i)));
             app *arg = to_app(ex->get_arg(i));
             get_len_exprs(arg, m_util_s, m, res);