From 1e5255508c0f0937c3db03f4ed79b185504a4fe3 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 26 Jul 2023 09:09:23 +0200
Subject: [PATCH] fixes

---
 src/math/dd/dd_pdd.h         |  4 ++--
 src/math/polysat/slicing.cpp | 18 +++++++++++-------
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 961c717cf..193fc3e3a 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -263,7 +263,7 @@ namespace dd {
         inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
         inline PDD hi(PDD p) const { return m_nodes[p].m_hi; }
         inline rational const& val(PDD p) const { SASSERT(is_val(p)); return m_values[lo(p)]; }
-        inline rational const& val_signed(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; }
+        inline rational get_signed_val(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; }
         inline void inc_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount++; SASSERT(!m_free_nodes.contains(p)); }
         inline void dec_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount--; SASSERT(!m_free_nodes.contains(p)); }
         inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
@@ -423,7 +423,7 @@ namespace dd {
         unsigned index() const { return root; }
         unsigned var() const { return m->var(root); }
         rational const& val() const { return m->val(root); }
-        rational const& val_signed() const { return m->val_signed(root); }
+        rational get_signed_val() const { return m->get_signed_val(root); }
         rational const& leading_coefficient() const;
         rational const& offset() const { return m->offset(root); }
         bool is_val() const { return m->is_val(root); }
diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index cf560cae9..fab000059 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -198,11 +198,12 @@ namespace polysat {
             case trail_item::split_core:
                 undo_split_core();
                 break;
-            case trail_item::mk_extract:
+            case trail_item::mk_extract: {
                 extract_args const& args = m_extract_trail.back();
                 replay_extract.push_back({args, m_extract_dedup[args]});
                 undo_mk_extract();
                 break;
+            }
             case trail_item::mk_concat:
                 num_replay_concat++;
                 break;
@@ -219,22 +220,25 @@ namespace polysat {
         unsigned concat_idx = m_concat_trail.size() - num_replay_concat;
         for (unsigned i = target_size; i < m_trail.size(); ++i) {
             switch (m_trail[i]) {
-            case trail_item::add_var:
+            case trail_item::add_var: {
                 unsigned const sz = replay_add_var[--add_var_idx];
-                add_var(replay_add_var[i]);
+                add_var(sz);
                 break;
+            }
             case trail_item::split_core:
                 /* do nothing */
                 break;
-            case trail_item::mk_extract:
+            case trail_item::mk_extract: {
                 auto const [args, v] = replay_extract[--extract_idx];
                 this->replay_extract(args, v);
                 break;
-            case trail_item::mk_concat:
-                auto ci = m_concat_trail[concat_idx++];
+            }
+            case trail_item::mk_concat: {
+                auto const ci = m_concat_trail[concat_idx++];
                 num_replay_concat++;
                 replay_concat(ci.num_args, &m_concat_args[ci.args_idx], ci.v);
                 break;
+            }
             default: UNREACHABLE();
             }
 
@@ -768,7 +772,7 @@ namespace polysat {
         get_base_core<true>(src, out_base);
     }
 
-    pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var = null_var) {
+    pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var) {
         enode_vector& slices = m_tmp3;
         SASSERT(slices.empty());
         mk_slice(src, hi, lo, slices, false, true);