diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp
index 447c2b2a1..ac13999d0 100644
--- a/src/smt/fingerprints.cpp
+++ b/src/smt/fingerprints.cpp
@@ -63,6 +63,26 @@ namespace smt {
 
     
     fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) {
+        
+        struct arg_data {
+            unsigned data_hash;
+            enode* const* args;
+        };
+        struct khash {
+            unsigned operator()(arg_data const& d) const {
+                return d.data_hash;
+            }
+        };
+        struct arghash {
+            unsigned operator()(arg_data const& d, unsigned i) const {
+                return d.args[i]->hash();
+            }
+        };
+        arg_data arg_data({ data_hash, args });
+        khash kh;
+        arghash ah;
+        data_hash = get_composite_hash(arg_data, num_args, kh, ah);
+
         fingerprint * d = mk_dummy(data, data_hash, num_args, args);
         if (m_set.contains(d)) 
             return nullptr;
@@ -107,8 +127,12 @@ namespace smt {
         unsigned new_lvl  = lvl - num_scopes;
         unsigned old_size = m_scopes[new_lvl];
         unsigned size     = m_fingerprints.size();
-        for (unsigned i = old_size; i < size; i++) 
-            m_set.erase(m_fingerprints[i]);
+        if (old_size == 0 && size > 0) 
+            m_set.reset();
+        else {
+            for (unsigned i = old_size; i < size; i++) 
+                m_set.erase(m_fingerprints[i]);
+        }
         m_fingerprints.shrink(old_size);
         m_defs.shrink(old_size);
         m_scopes.shrink(new_lvl);
diff --git a/src/smt/fingerprints.h b/src/smt/fingerprints.h
index b1904a4ee..a602f25cd 100644
--- a/src/smt/fingerprints.h
+++ b/src/smt/fingerprints.h
@@ -48,15 +48,9 @@ namespace smt {
     
     class fingerprint_set {
         
-        struct fingerprint_khasher {
-            unsigned operator()(fingerprint const * f) const { return f->get_data_hash(); }
-        };
-        struct fingerprint_chasher {
-            unsigned operator()(fingerprint const * f, unsigned idx) const { return f->get_arg(idx)->hash(); }
-        };
         struct fingerprint_hash_proc {
             unsigned operator()(fingerprint const * f) const {
-                return get_composite_hash<fingerprint *, fingerprint_khasher, fingerprint_chasher>(const_cast<fingerprint*>(f), f->get_num_args());
+                return f->get_data_hash();
             }
         };
         struct fingerprint_eq_proc { bool operator()(fingerprint const * f1, fingerprint const * f2) const; };