diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index e699ee356..369c3aae6 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -252,7 +252,7 @@ public:
                 bool found = false;
                 for (unsigned i = 1; !found && i < parents.size(); ++i) {
                     if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
-                        parents[1] = parents[i];
+                        parents[1] = parents[i].get();
                         parents.resize(2);
                         result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
                         m_refs.push_back(result);