diff --git a/src/test/total_order.cpp b/src/test/total_order.cpp
index 99c54fb8dd..3d879030a4 100644
--- a/src/test/total_order.cpp
+++ b/src/test/total_order.cpp
@@ -50,6 +50,8 @@ static void tst2() {
 }
 
 static void tst3(unsigned sz, unsigned num_rounds) {
+    if (sz == 0)
+        return;
     uint_total_order to;
     to.insert(0);
     for (unsigned i = 0; i < sz; ++i) {
@@ -100,6 +102,8 @@ void move_after(unsigned_vector & v, unsigned_vector & inv_v, unsigned a, unsign
 }
 
 static void tst4(unsigned sz, unsigned num_rounds) {
+    if (sz == 0)
+        return;
     uint_total_order to;
     unsigned_vector  v;
     unsigned_vector  inv_v;
diff --git a/src/test/var_subst.cpp b/src/test/var_subst.cpp
index 36d5e8f039..04667b73fa 100644
--- a/src/test/var_subst.cpp
+++ b/src/test/var_subst.cpp
@@ -33,7 +33,7 @@ namespace find_q {
         void operator()(app * n) {}
         void operator()(quantifier * n) { m_q = n; }
     };
-};
+}
 
 quantifier * find_quantifier(expr * n) {
     find_q::proc p;
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 705fae5092..f3f5ae6b24 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -17,6 +17,8 @@ Revision History:
 
 --*/
 #include<cstdio>
+#include<cstdlib>
+#include<csignal>
 #ifndef _WINDOWS
 #include<unistd.h>
 #endif
@@ -185,9 +187,13 @@ debug_action ask_debug_action(std::istream& in) {
 }
 
 #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
+[[noreturn]] static void force_segfault() {
+    std::raise(SIGSEGV);
+    std::abort();
+}
+
 void invoke_debugger() {
     std::string buffer;
-    int *x = nullptr;
     debug_action a = get_default_debug_action();
     for (;;) {
         switch (a) {
@@ -197,8 +203,7 @@ void invoke_debugger() {
             exit(1);
         case debug_action::stop:
             // force seg fault...
-            *x = 0;
-            return;
+            force_segfault();
         case debug_action::throw_exception:
             throw default_exception("assertion violation");
         case debug_action::invoke_gdb:
@@ -210,8 +215,7 @@ void invoke_debugger() {
             else {
                 std::cerr << "error starting GDB...\n";
                 // forcing seg fault.
-                int *x = nullptr;
-                *x = 0;
+                force_segfault();
             }
             return;
         case debug_action::invoke_lldb:
@@ -223,8 +227,7 @@ void invoke_debugger() {
             else {
                 std::cerr << "error starting LLDB...\n";
                 // forcing seg fault.
-                int *x = nullptr;
-                *x = 0;
+                force_segfault();
             }
             return;
         case debug_action::ask:
diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp
index c2c0586961..e4031507fc 100644
--- a/src/util/mpff.cpp
+++ b/src/util/mpff.cpp
@@ -158,24 +158,26 @@ bool mpff_manager::is_uint64(mpff const & n) const {
 uint64_t mpff_manager::get_uint64(mpff const & a) const {
     SASSERT(is_uint64(a));
     if (is_zero(a)) return 0;
-    int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
+    int64_t exp = -static_cast<int64_t>(a.m_exponent) - sizeof(unsigned) * 8 * (m_precision - 2);
     SASSERT(exp >= 0);
+    SASSERT(exp < 64);
     uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
-    return *s >> static_cast<unsigned>(exp);
+    return exp < 64 ? *s >> static_cast<unsigned>(exp) : 0;
 }
 
 int64_t mpff_manager::get_int64(mpff const & a) const {
     SASSERT(is_int64(a));
     if (is_zero(a)) return 0;
-    int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
+    int64_t exp = -static_cast<int64_t>(a.m_exponent) - sizeof(unsigned) * 8 * (m_precision - 2);
     SASSERT(exp >= 0);
+    SASSERT(exp < 64);
     uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
     // INT64_MIN case
     if (exp == 0 && *s == 0x8000000000000000ull && is_neg(a)) {
         return INT64_MIN;
     }
     else {
-        int64_t r = *s >> static_cast<unsigned>(exp);
+        int64_t r = exp < 64 ? *s >> static_cast<unsigned>(exp) : 0;
         if (is_neg(a))
             r = -r;
         return r;
diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h
index 0a91f7a85e..c524e344b7 100644
--- a/src/util/sorting_network.h
+++ b/src/util/sorting_network.h
@@ -224,7 +224,7 @@ Notes:
             }
         };
 
-        psort_nw(psort_expr& c): ctx(c) {}
+        psort_nw(psort_expr& c): ctx(c), m_t(GE) {}
 
         sorting_network_config& cfg() { return m_cfg; }
 
@@ -1497,4 +1497,3 @@ Notes:
             }
         }
     };
-