From 16af728fbe0cb3fd7583d921fea9b545f42591b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 May 2019 23:27:35 -0700 Subject: [PATCH] fix #2263 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 175fe87fc..edbc11e7d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1799,13 +1799,13 @@ namespace z3 { unsigned m_index; public: iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {} - iterator(iterator& other): m_vector(other.m_vector), m_index(other.m_index) {} + iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {} iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; } - bool operator==(iterator const& other) { + bool operator==(iterator const& other) const { return other.m_index == m_index; }; - bool operator!=(iterator const& other) { + bool operator!=(iterator const& other) const { return other.m_index != m_index; }; iterator& operator++() {