From f11cb77c3d00bfe63b38e8ee0ed0d00027cf44ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 May 2019 16:15:55 -0700
Subject: [PATCH] merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/shell/main.cpp | 2 --
 src/util/mpz.cpp   | 7 ++++---
 2 files changed, 4 insertions(+), 5 deletions(-)

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);