diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 42f989a8a..fb586cafb 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -377,9 +377,11 @@ namespace {
 
                 for (expr* c : core) {
                     expr_ref name(c, m);
-                    SASSERT(m_name2assertion.contains(name));
-                    expr_ref assrtn(m_name2assertion.find(name), m);
-                    collect_pattern_fds(assrtn, pattern_fds);
+                    expr* f = nullptr;
+                    if (m_name2assertion.find(name, f)) {
+                        expr_ref assrtn(f, m);
+                        collect_pattern_fds(assrtn, pattern_fds);
+                    }
                 }
 
                 if (!pattern_fds.empty()) {
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 2edb4a518..30372ab6b 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1781,8 +1781,9 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
 }
 
 static void display_binary_data(std::ostream &out, uint64_t val, uint64_t numBits) {
-	for (uint64_t shift = numBits; shift-- > 64ull; ) out << "0";
-    for (uint64_t shift = std::min(64ull, numBits); shift-- > 0; ) {
+    for (uint64_t shift = numBits; shift-- > 64ull; ) out << "0";
+    if (numBits > 64) numBits = 64;
+    for (uint64_t shift = numBits; shift-- > 0; ) {
         if (val & (1ull << shift)) {
             out << "1";
         } else {