diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 641c01285..8bd125dd7 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -218,6 +218,7 @@ unsigned decl_info::hash() const {
 
 bool decl_info::operator==(decl_info const & info) const {
     return m_family_id == info.m_family_id && m_kind == info.m_kind &&
+        m_parameters.size() == info.m_parameters.size() && 
         compare_arrays<parameter>(m_parameters.begin(), info.m_parameters.begin(), m_parameters.size());
 }
 
diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp
index 48fd7d69a..a7b2dfd53 100644
--- a/src/smt/old_interval.cpp
+++ b/src/smt/old_interval.cpp
@@ -235,6 +235,7 @@ interval::interval(interval const & other):
     m_upper_open(other.m_upper_open),
     m_lower_dep(other.m_lower_dep),
     m_upper_dep(other.m_upper_dep) {
+    std::cout << "copy " << m_lower << " " << m_upper << "\n";
 }
 
 interval & interval::operator=(interval const & other) {
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index d75ab0f13..79e317e44 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1995,6 +1995,7 @@ bool theory_arith<Ext>::is_inconsistent2(grobner::equation const * eq, grobner &
         grobner::monomial const * m = eq->get_monomial(i);
         intervals.push_back(mk_interval_for(m));
     }
+    std::cout << intervals.size() << "\n";
     sbuffer<bool> deleted;
     deleted.resize(num, false);
     ptr_buffer<grobner::monomial> monomials;