diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index bb148d712..85d5fce62 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1603,10 +1603,10 @@ namespace z3 {
             unsigned i;
         public:
             iterator(expr& e, unsigned i): e(e), i(i) {}
-            bool operator==(iterator const& other) noexcept {
+            bool operator==(iterator const& other) const noexcept {
                 return i == other.i;
             }
-            bool operator!=(iterator const& other) noexcept {
+            bool operator!=(iterator const& other) const noexcept {
                 return i != other.i;
             }
             expr operator*() const { return e.arg(i); }
@@ -1703,28 +1703,28 @@ namespace z3 {
 
     inline expr operator||(bool a, expr const & b) { return b.ctx().bool_val(a) || b; }
 
-    inline expr operator==(expr const & a, expr const & b) {
+    inline expr operator==(expr const & a, expr const & b) const {
         check_context(a, b);
         Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
         a.check_error();
         return expr(a.ctx(), r);
     }
-    inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
+    inline expr operator==(expr const & a, int b) const { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
     inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
-    inline expr operator==(expr const & a, double b) { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
-    inline expr operator==(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
+    inline expr operator==(expr const & a, double b) const { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }
+    inline expr operator==(double a, expr const & b) const { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }
 
-    inline expr operator!=(expr const & a, expr const & b) {
+    inline expr operator!=(expr const & a, expr const & b) const {
         check_context(a, b);
         Z3_ast args[2] = { a, b };
         Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
         a.check_error();
         return expr(a.ctx(), r);
     }
-    inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
-    inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
-    inline expr operator!=(expr const & a, double b) { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
-    inline expr operator!=(double a, expr const & b) { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
+    inline expr operator!=(expr const & a, int b) const { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
+    inline expr operator!=(int a, expr const & b) const { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
+    inline expr operator!=(expr const & a, double b) const { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }
+    inline expr operator!=(double a, expr const & b) const { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }
 
     inline expr operator+(expr const & a, expr const & b) {
         check_context(a, b);
@@ -2957,10 +2957,10 @@ namespace z3 {
             expr_vector const * operator->() const { return &(operator*()); }
             expr_vector const& operator*() const noexcept { return m_cube; }
 
-            bool operator==(cube_iterator const& other) noexcept {
+            bool operator==(cube_iterator const& other) const noexcept {
                 return other.m_end == m_end;
             };
-            bool operator!=(cube_iterator const& other) noexcept {
+            bool operator!=(cube_iterator const& other) const noexcept {
                 return other.m_end != m_end;
             };
 
diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h
index 158df4906..d1d946d10 100644
--- a/src/muz/rel/dl_base.h
+++ b/src/muz/rel/dl_base.h
@@ -1113,7 +1113,7 @@ namespace datalog {
 
             virtual row_interface & operator*() = 0;
             virtual void operator++() = 0;
-            virtual bool operator==(const iterator_core & it) {
+            virtual bool operator==(const iterator_core & it) const {
                 //we worry about the equality operator only because of checking
                 //the equality with the end() iterator
                 return is_finished() && it.is_finished();
@@ -1142,7 +1142,7 @@ namespace datalog {
 
             virtual table_element operator*() = 0;
             virtual void operator++() = 0;
-            virtual bool operator==(const row_iterator_core & it) {
+            virtual bool operator==(const row_iterator_core & it) const {
                 //we worry about the equality operator only because of checking
                 //the equality with the end() iterator
                 return is_finished() && it.is_finished();
@@ -1169,10 +1169,8 @@ namespace datalog {
             { return &(*(*m_core)); }
             iterator & operator++()
             { ++(*m_core); return *this; }
-            bool operator==(const iterator & it)
-            { return (*m_core)==(*it.m_core); }
-            bool operator!=(const iterator & it)
-            { return !operator==(it); }
+            bool operator==(const iterator & it) const  { return (*m_core)==(*it.m_core); }
+            bool operator!=(const iterator & it) const  { return !operator==(it); }
         };
 
         class row_iterator {
@@ -1187,10 +1185,8 @@ namespace datalog {
             { return *(*m_core); }
             row_iterator & operator++()
             { ++(*m_core); return *this; }
-            bool operator==(const row_iterator & it)
-            { return (*m_core)==(*it.m_core); }
-            bool operator!=(const row_iterator & it)
-            { return !operator==(it); }
+            bool operator==(const row_iterator & it) const  { return (*m_core)==(*it.m_core); }
+            bool operator!=(const row_iterator & it) const  { return !operator==(it); }
         };
 
         virtual iterator begin() const = 0;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 19482c286..5e0d10918 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -179,8 +179,6 @@ public:
     void initialize_values() {
         if (m_mcs.back())
             m_mcs.back()->convert_initialize_value(m_var2value);
-        if (m_mcs.back())
-            m_mcs.back()->display(verbose_stream());
 
         for (auto & [var, value] : m_var2value) {
             sat::bool_var b = m_map.to_bool_var(var);
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index e997cbc2c..6a48bc8ed 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -265,7 +265,6 @@ public:
     }
 
     void user_propagate_initialize_value(expr* var, expr* value) override {
-        verbose_stream() << "initialize-value\n";
         m_var2value.push_back({ expr_ref(var, m), expr_ref(value, m) });
     }