diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 756633048..d03b6c445 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -81,7 +81,6 @@ namespace api {
         m_fpa_util(m()),
         m_sutil(m()),
         m_recfun(m()),
-        m_last_result(m()),
         m_ast_trail(m()),
         m_pmanager(m_limit) {
 
@@ -226,12 +225,12 @@ namespace api {
     void context::save_ast_trail(ast * n) {
         SASSERT(m().contains(n));
         if (m_user_ref_count) {
-            // Corner case bug: n may be in m_last_result, and this is the only reference to n.
+            // Corner case bug: n may be in m_ast_trail, and this is the only reference to n.
             // When, we execute reset() it is deleted
-            // To avoid this bug, I bump the reference counter before resetting m_last_result
+            // To avoid this bug, I bump the reference counter before resetting m_ast_trail
             ast_ref node(n, m());
-            m_last_result.reset();
-            m_last_result.push_back(std::move(node));
+            m_ast_trail.reset();
+            m_ast_trail.push_back(std::move(node));
         }
         else {
             m_ast_trail.push_back(n);
@@ -239,15 +238,12 @@ namespace api {
     }
 
     void context::save_multiple_ast_trail(ast * n) {
-        if (m_user_ref_count)
-            m_last_result.push_back(n);
-        else
-            m_ast_trail.push_back(n);
+        m_ast_trail.push_back(n);
     }
 
     void context::reset_last_result() {
         if (m_user_ref_count)
-            m_last_result.reset();
+            m_ast_trail.reset();
         m_last_obj = nullptr;
     }
 
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 83f569767..d0f31c589 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -91,8 +91,7 @@ namespace api {
         smt_params                 m_fparams;
         // -------------------------------
 
-        ast_ref_vector             m_last_result; //!< used when m_user_ref_count == true
-        ast_ref_vector             m_ast_trail;   //!< used when m_user_ref_count == false
+        ast_ref_vector             m_ast_trail;
 
         ref<api::object>           m_last_obj; //!< reference to the last API object returned by the APIs
         u_map<api::object*>        m_allocated_objects; // !< table containing current set of allocated API objects