Merge branch 'master' into nlsat-solver-stack

Z3Prover · Aug 26, 2024 · d263714 · d263714
2 parents 3656a26 + 6a68cc5
commit d263714
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 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
@@ -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));