From 6a68cc55bbefcac1fdb417260850af9a84717260 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Aug 2024 09:59:50 -0700 Subject: [PATCH] #7353 - clear pointer when existing stack Signed-off-by: Nikolaj Bjorner --- src/sat/sat_ddfw.cpp | 2 +- src/tactic/arith/fix_dl_var_tactic.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index bd7b0d26cbf..ccf5a55db2c 100644 --- 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 index 13479e1bffe..c96ca749b90 100644 --- 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 m_todo; obj_map m_occs; obj_map 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 _visited(m_visited, &visited); unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { process(g.form(i));