fix warning with iterators due to non-const comparator

Z3Prover · Sep 23, 2024 · 22d9bfa · 22d9bfa
1 parent 1121815
commit 22d9bfa
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/src/ast/rewriter/factor_equivs.h b/src/ast/rewriter/factor_equivs.h
@@ -103,11 +103,10 @@ class obj_equiv_class {
             m_first = false;
             return *this;
         }
-        bool operator==(const iterator& o) {
+        bool operator!=(const iterator& o) const {
             SASSERT(&m_ouf == &o.m_ouf);
-            return  m_first == o.m_first && m_curr_id == o.m_curr_id;
+            return  m_first != o.m_first || m_curr_id != o.m_curr_id;
         }
-        bool operator!=(const iterator& o) {return !(*this == o);}
     };
 
     iterator begin(OBJ*o) {
@@ -152,11 +151,10 @@ class obj_equiv_class {
                     m_ouf.m_uf.is_root(m_rootnb) != true);
             return *this;
         }
-        bool operator==(const equiv_iterator& o) {
+        bool operator!=(const equiv_iterator& o) const {
             SASSERT(&m_ouf == &o.m_ouf);
-            return m_rootnb == o.m_rootnb;
+            return m_rootnb != o.m_rootnb;
         }
-        bool operator!=(const equiv_iterator& o) {return !(*this == o);}
     };
 
     equiv_iterator begin() {return equiv_iterator(*this, 0);}