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 39a6c1af6d6..c96ca749b90 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -214,10 +214,8 @@ class fix_dl_var_tactic : public tactic {
 
         app * operator()(goal const & g) {
             try {
-                if (m_visited != nullptr) {
-                    dealloc(m_visited);
-                }
-                m_visited = alloc(expr_fast_mark1);
+                expr_fast_mark1 visited;
+                flet<expr_fast_mark1*> _visited(m_visited, &visited);
                 unsigned sz = g.size();
                 for (unsigned i = 0; i < sz; i++) {
                     process(g.form(i));