diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index bf247d1f9..da676aac9 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -168,9 +168,9 @@ namespace polysat {
     }
 
     void slicing::undo_merge_base() {
-        slice r1 = m_merge_trail.back();
+        auto const [r1, s1] = m_merge_trail.back();
         m_merge_trail.pop_back();
-        slice r2 = m_find[r1];
+        slice const r2 = m_find[r1];
         SASSERT(find(r2) == r2);
         m_find[r1] = r1;
         m_size[r2] -= m_size[r1];
diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h
index f044a69d4..19b191d4e 100644
--- a/src/math/polysat/types.h
+++ b/src/math/polysat/types.h
@@ -36,7 +36,8 @@ namespace polysat {
     typedef dd::bddv bddv;
     typedef dd::val_pp val_pp;
 
-    typedef unsigned pvar;
+    using pvar = unsigned;
+    using pvar_vector = unsigned_vector;
     inline const pvar null_var = UINT_MAX;
 
     class dependency {
@@ -49,7 +50,7 @@ namespace polysat {
     };
 
     inline const dependency null_dependency = dependency(UINT_MAX);
-    typedef svector<dependency> dependency_vector;
+    using dependency_vector = svector<dependency>;
 
     inline bool operator< (dependency const& d1, dependency const& d2) { return d1.val() <  d2.val(); }
     inline bool operator<=(dependency const& d1, dependency const& d2) { return d1.val() <= d2.val(); }