fix non-termination bug in elim-unconstrained, add parameter validati…

…on to fix #7432
Z3Prover · Oct 22, 2024 · 253f7d7 · 253f7d7
1 parent d18831c
commit 253f7d7
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 8 deletions.
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -86,7 +86,7 @@ void elim_unconstrained::eliminate() {
             continue;
         }
         if (m_heap.contains(root(e))) {
-            IF_VERBOSE(11, verbose_stream() << "already in heap " << mk_bounded_pp(e, m) << "\n");
+            TRACE("elim_unconstrained", tout << "already in heap " << mk_bounded_pp(e, m) << "\n");
             continue;
         }
         app* t = to_app(e);
@@ -111,9 +111,9 @@ void elim_unconstrained::eliminate() {
             continue;
         }
 
-        IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " : " << rr << " -> " << r << "\n");
+        IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
 
-        TRACE("elim_unconstrained", tout << mk_pp(t, m) << " : " << rr << " -> " << r << "\n");
+        TRACE("elim_unconstrained", tout << mk_pp(t, m) << " / " << rr << " -> " << r << "\n");
         SASSERT(r->get_sort() == t->get_sort());
         m_stats.m_num_eliminated++;
         m_trail.push_back(r);
@@ -147,10 +147,10 @@ expr* elim_unconstrained::get_parent(unsigned n) const {
 }
 
 void elim_unconstrained::invalidate_parents(expr* e) {
-    ptr_vector<expr> todo;
+    ptr_buffer<expr> todo;
     do {
         node& n = get_node(e);
-        if (!n.m_dirty) {
+        if (!n.m_dirty && e == n.m_term) {
             n.m_dirty = true;
             for (expr* e : n.m_parents)
                 todo.push_back(e);            
@@ -299,7 +299,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
         return expr_ref(t, m);
     if (!is_node(t))
         return expr_ref(t, m);
-    ptr_vector<expr> todo;
+    ptr_buffer<expr> todo;
     todo.push_back(t);
     while (!todo.empty()) {
         t = todo.back();
@@ -310,6 +310,7 @@ expr_ref elim_unconstrained::reconstruct_term(node& n0) {
         unsigned sz0 = todo.size();
         if (is_app(t)) {     
             if (n.m_term != t) {
+                n.m_dirty = false;
                 todo.pop_back();
                 continue;
             }

diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
@@ -225,7 +225,9 @@ class psort_app : public psort {
             sort * a = m_args[i]->instantiate(m, n, s);
             args_i.push_back(a);
         }
-        r = m_decl->instantiate(m, args_i.size(), args_i.data());        
+        r = m_decl->instantiate(m, args_i.size(), args_i.data());  
+        if (m_num_params != n)
+            throw default_exception("mismatch between number of declared and supplied sort parameters");
         cache(m, s, r);
         return r;
     }
@@ -771,6 +773,8 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
         for (unsigned i = 0; i < d->get_num_params(); ++i) {
             ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr));
         }        
+        verbose_stream() << ps.size() << " " << ps << "\n";
+
         dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.data()));
     }
     sort_ref_vector sorts(m.m());

diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
@@ -262,7 +262,6 @@ namespace sat {
         m_assumptions.append(sz, assumptions);
         add_assumptions();
         for (unsigned v = 0; v < num_vars(); ++v) {
-            literal lit(v, false), nlit(v, true);
             value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size();
         }
         init_clause_data();