diff --git a/src/tests/util/pdeque.cpp b/src/tests/util/pdeque.cpp
index 073ffa247..5ae57bcbe 100644
--- a/src/tests/util/pdeque.cpp
+++ b/src/tests/util/pdeque.cpp
@@ -76,6 +76,13 @@ static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double p
         double f = static_cast<double>(std::rand() % 10000) / 10000.0;
         if (f < copy_freq)
             copies.push_back(q3);
+        // read random positions of q3
+        if (!empty(q3)) {
+            for (unsigned j = 0; j < rand() % 5; j++) {
+                unsigned idx = rand() % size(q3);
+                lean_assert(q3[idx] == q1[idx]);
+            }
+        }
         f = static_cast<double>(std::rand() % 10000) / 10000.0;
         if (f < push_freq) {
             if (q1.size() >= max_sz)
diff --git a/src/tests/util/pvector.cpp b/src/tests/util/pvector.cpp
index 7babeb9f6..c792b7ff4 100644
--- a/src/tests/util/pvector.cpp
+++ b/src/tests/util/pvector.cpp
@@ -50,29 +50,53 @@ bool operator==(pvector<T> v1, std::vector<T> const & v2) {
     return true;
 }
 
+template<typename T>
+bool operator==(pvector<T> v1, pvector<T> v2) {
+    if (v1.size() != v2.size())
+        return false;
+    for (unsigned i = 0; i < v1.size(); i++) {
+        if (v1[i] != v2[i])
+            return false;
+    }
+    return true;
+}
+
 static void driver(unsigned max_sz, unsigned max_val, unsigned num_ops, double push_freq, double copy_freq) {
     std::vector<int> v1;
     pvector<int>     v2;
+    pvector<int>     v3;
     std::vector<pvector<int>> copies;
     for (unsigned i = 0; i < num_ops; i++) {
         double f = static_cast<double>(std::rand() % 10000) / 10000.0;
-        if (f < copy_freq)
+        if (f < copy_freq) {
             copies.push_back(v2);
+        }
         f = static_cast<double>(std::rand() % 10000) / 10000.0;
+        // read random positions of v3
+        if (!empty(v3)) {
+            for (unsigned j = 0; j < rand() % 5; j++) {
+                unsigned idx = rand() % size(v3);
+                lean_assert(v3[idx] == v1[idx]);
+            }
+        }
         if (f < push_freq) {
             if (v1.size() >= max_sz)
                 continue;
             int a = std::rand() % max_val;
             v1.push_back(a);
             v2.push_back(a);
+            v3 = push_back(v3, a);
+            lean_assert(back(v3) == a);
         } else {
             if (v1.size() == 0)
                 continue;
             lean_assert(v1.back() == v2.back());
             v1.pop_back();
             v2.pop_back();
+            v3 = pop_back(v3);
         }
         lean_assert(v2 == v1);
+        lean_assert(v3 == v1);
     }
     std::cout << "Copies created: " << copies.size() << "\n";
 }
@@ -113,6 +137,42 @@ static void tst3() {
     for (unsigned i = 0; i < M; i++) { s += v2[i % v2.size()]; }
 }
 
+static void tst4() {
+    pvector<int> v;
+    lean_assert(empty(v));
+    lean_assert(size(v) == 0);
+    v = push_back(v, 1);
+    lean_assert(size(v) == 1);
+    std::cout << "v: " << v << "\n";
+    lean_assert(back(v) == 1);
+    lean_assert(!empty(v));
+    v = push_back(v, 2);
+    lean_assert(back(v) == 2);
+    std::cout << "v: " << v << "\n";
+    v = push_back(v, 3);
+    std::cout << "v: " << v << "\n";
+    lean_assert(size(v) == 3);
+    lean_assert(v[0] == 1);
+    lean_assert(back(v) == 3);
+    lean_assert(size(pop_back(v)) == 2);
+    lean_assert(back(pop_back(v)) == 2);
+    lean_assert(pop_back(pop_back(v))[0] == 1);
+    lean_assert(empty(pop_back(pop_back(pop_back(v)))));
+    lean_assert(pop_back(push_back(v, 3)) == v);
+}
+
+static void tst5() {
+    pvector<int> v;
+    v.push_back(0);
+    pvector<int> v2 = v;
+    for (unsigned i = 1; i < 100; i++) {
+        lean_assert(v2[0] == 0);
+        v2.push_back(i);
+        lean_assert(v2[0] == 0);
+        v = pvector<int>();
+    }
+}
+
 #ifdef PVECTOR_PERF_TEST
 static void perf_vector(unsigned n) {
     std::vector<int> q;
@@ -188,6 +248,8 @@ int main() {
     tst1();
     tst2();
     tst3();
+    tst4();
+    tst5();
 #ifdef PVECTOR_PERF_TEST
     tst_perf1();
     tst_perf2();
diff --git a/src/util/pdeque.h b/src/util/pdeque.h
index a91dcfa07..c62cef637 100644
--- a/src/util/pdeque.h
+++ b/src/util/pdeque.h
@@ -533,7 +533,7 @@ template<typename T>
 unsigned size(pdeque<T> const & s) { return s.size(); }
 
 template<typename T> inline std::ostream & operator<<(std::ostream & out, pdeque<T> const & d) {
-    out << "[";
+    out << "[[";
     bool first = true;
     auto it  = d.begin();
     auto end = d.end();
@@ -541,10 +541,10 @@ template<typename T> inline std::ostream & operator<<(std::ostream & out, pdeque
         if (first)
             first = false;
         else
-            out << " ";
+            out << ", ";
         out << *it;
     }
-    out << "]";
+    out << "]]";
     return out;
 }
 }
diff --git a/src/util/pvector.h b/src/util/pvector.h
index a60bbbae3..2b5a3ab1d 100644
--- a/src/util/pvector.h
+++ b/src/util/pvector.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <iostream>
 #include <vector>
 #include "rc.h"
 
@@ -173,12 +174,17 @@ class pvector {
         }
     }
 
-    /** \brief Update quota based on the cost of a read */
-    void update_quota_on_read(unsigned cost) {
+    /**
+        \brief Update quota based on the cost of a read
+        Return true if the quota was updated, and false
+        if the representation had to be updated.
+    */
+    bool update_quota_on_read(unsigned cost) {
         cost /= 2; // reads are cheaper than writes
         if (cost > 0) {
             if (cost >= m_ptr->quota()) {
                 flat();
+                return false;
             } else {
                 if (is_shared()) {
                     switch (m_ptr->kind()) {
@@ -193,6 +199,7 @@ class pvector {
                 static_cast<delta_cell*>(m_ptr)->m_quota -= cost;
             }
         }
+        return true;
     }
 
     void pop_back_core() { update_cell(new pop_cell(m_ptr)); }
@@ -230,21 +237,27 @@ public:
             switch (it->kind()) {
             case cell_kind::PushBack:
                 if (i + 1 == to_push(it).m_size) {
-                    const_cast<pvector*>(this)->update_quota_on_read(cost);
-                    return to_push(it).m_val;
+                    if (const_cast<pvector*>(this)->update_quota_on_read(cost))
+                        return to_push(it).m_val;
+                    else
+                        return operator[](i); // representation was changed, \c it may have been deleted
                 }
                 break;
             case cell_kind::PopBack:
                 break;
             case cell_kind::Set:
                 if (to_set(it).m_idx == i) {
-                    const_cast<pvector*>(this)->update_quota_on_read(cost);
-                    return to_set(it).m_val;
+                    if (const_cast<pvector*>(this)->update_quota_on_read(cost))
+                        return to_set(it).m_val;
+                    else
+                        return operator[](i); // representation was changed, \c it may have been deleted
                 }
                 break;
             case cell_kind::Root:
-                const_cast<pvector*>(this)->update_quota_on_read(cost);
-                return to_root(it).m_vector[i];
+                if (const_cast<pvector*>(this)->update_quota_on_read(cost))
+                    return to_root(it).m_vector[i];
+                else
+                    return operator[](i); // representation was changed, \c it may have been deleted
             }
             it = static_cast<delta_cell const *>(it)->m_prev;
             cost++;
@@ -332,6 +345,7 @@ public:
     }
 
     class iterator {
+        friend class pvector;
         pvector const & m_vector;
         unsigned        m_it;
         iterator(pvector const & v, unsigned it):m_vector(v), m_it(it) {}
@@ -341,8 +355,8 @@ public:
         iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; }
         bool operator==(iterator const & s) const { lean_assert(&m_vector == &(s.m_vector)); return m_it == s.m_it; }
         bool operator!=(iterator const & s) const { return !operator==(s); }
-        T const & operator*() { lean_assert(m_it); return m_vector[m_it]; }
-        T const * operator->() { lean_assert(m_it); return &(m_vector[m_it]); }
+        T const & operator*() const { return m_vector[m_it]; }
+        T const * operator->() const { return &(m_vector[m_it]); }
     };
 
     /** \brief Return an iterator to the beginning */
@@ -405,4 +419,23 @@ T const & back(pvector<T> const & s) { return s.back(); }
 /** \brief Return true iff \c s is empty. */
 template<typename T>
 bool empty(pvector<T> const & s) { return s.empty(); }
+/** \brief Return the size of \c s. */
+template<typename T>
+unsigned size(pvector<T> const & s) { return s.size(); }
+
+template<typename T> inline std::ostream & operator<<(std::ostream & out, pvector<T> const & d) {
+    out << "[";
+    bool first = true;
+    auto it  = d.begin();
+    auto end = d.end();
+    for (; it != end; ++it) {
+        if (first)
+            first = false;
+        else
+            out << ", ";
+        out << *it;
+    }
+    out << "]";
+    return out;
+}
 }