From bec38f268b51940adec2e38686b32e0287fb105c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 1 Aug 2019 16:32:08 +0800
Subject: [PATCH] remove debug code

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/params.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/util/params.cpp b/src/util/params.cpp
index dcb2c80cc..3edc7d329 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -339,8 +339,6 @@ public:
     void inc_ref() { m_ref_count++; }
     void dec_ref() { 
         SASSERT(m_ref_count > 0);
-        if (m_ref_count > 10000) 
-            IF_VERBOSE(0, verbose_stream() << this << " " << m_ref_count << " " << std::this_thread::get_id() << "\n";);
         if (--m_ref_count == 0) dealloc(this); 
     }