#7353 - clear pointer when existing stack

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 26, 2024 · 6a68cc5 · 6a68cc5
1 parent c1454dc
commit 6a68cc5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
@@ -613,7 +613,7 @@ namespace sat {
             out << ci.m_num_trues << " " << ci.m_weight << "\n";
         }
         for (unsigned v = 0; v < num_vars(); ++v) {
-            out << v << ": " << reward(v) << "\n";
+            out << v << ": rw " << reward(v) << "\n";
         }
         out << "unsat vars: ";
         for (bool_var v : m_unsat_vars) {

diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -35,7 +35,7 @@ class fix_dl_var_tactic : public tactic {
         struct failed {};
         ast_manager &          m;
         arith_util &           m_util;
-        expr_fast_mark1 *      m_visited;
+        expr_fast_mark1 *      m_visited = nullptr;
         ptr_vector<expr>       m_todo;
         obj_map<app, unsigned> m_occs;
         obj_map<app, unsigned> m_non_nested_occs;
@@ -215,7 +215,7 @@ class fix_dl_var_tactic : public tactic {
         app * operator()(goal const & g) {
             try {
                 expr_fast_mark1 visited;
-                m_visited = &visited;
+                flet<expr_fast_mark1*> _visited(m_visited, &visited);
                 unsigned sz = g.size();
                 for (unsigned i = 0; i < sz; i++) {
                     process(g.form(i));