remove debug code

NikolajBjorner · NikolajBjorner · commit bec38f268b51 · 2019-08-01T16:32:08.000+08:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/util/params.cpp b/src/util/params.cpp
@@ -339,8 +339,6 @@ class params {
     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); 
     }
 

Original file line number	Diff line number	Diff line change
`@@ -339,8 +339,6 @@ class params {`
`339`	`339`	`void inc_ref() { m_ref_count++; }`
`340`	`340`	`void dec_ref() {`
`341`	`341`	`SASSERT(m_ref_count > 0);`
`342`		`- if (m_ref_count > 10000)`
`343`		`- IF_VERBOSE(0, verbose_stream() << this << " " << m_ref_count << " " << std::this_thread::get_id() << "\n";);`
`344`	`342`	`if (--m_ref_count == 0) dealloc(this);`
`345`	`343`	`}`
`346`	`344`