From 22d9bfad358eefaa2f7aa490983463f6b0dd022f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 23 Sep 2024 08:10:56 +0100 Subject: [PATCH] fix warning with iterators due to non-const comparator --- src/ast/rewriter/factor_equivs.h | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/factor_equivs.h b/src/ast/rewriter/factor_equivs.h index 7c58f4abde8..d4d566ed6fe 100644 --- 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);}