From 8e83d04e027f9a7b9c5c1e3539c8363ae711a549 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Nov 2018 14:22:22 -0800 Subject: [PATCH] this->size() Signed-off-by: Nikolaj Bjorner --- src/util/ref_vector.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index b259cd468..d0e9a8f55 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -307,8 +307,8 @@ public: ref_vector & operator=(ref_vector const & other) = delete; bool operator==(ref_vector const& other) const { - if (other.size() != size()) return false; - for (unsigned i = size(); i-- > 0; ) { + if (other.size() != this->size()) return false; + for (unsigned i = this->size(); i-- > 0; ) { if (other[i] != (*this)[i]) return false; } return true;