diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 68b807f87a3..1718e7314d6 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -262,13 +262,11 @@ static void parse_cmd_line_args(int argc, char ** argv) {
                 enable_trace(opt_arg);
             }
 #endif
-#ifdef Z3DEBUG
             else if (strcmp(opt_name, "dbg") == 0) {
                 if (!opt_arg)
                     error("option argument (-dbg:tag) is missing.");
                 enable_debug(opt_arg);
             }
-#endif
             else if (strcmp(opt_name, "memory") == 0) {
                 if (!opt_arg)
                     error("option argument (-memory:val) is missing.");
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 178d5042dd4..1e74c2e9eff 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1783,9 +1783,10 @@ void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
 
 template<bool SYNCH>
 void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const {
-    if (is_small(a)) {
-        display_binary_data(out, static_cast<unsigned>(get_uint64(a)), num_bits);
-    } else {
+    if (is_uint(a)) {
+        display_binary_data(out, get_uint(a), num_bits);
+    } 
+    else {
 #ifndef _MP_GMP
         digit_t *ds = digits(a);
         unsigned sz = size(a);