From 3d9120c74503171c00838f64fe73bb91c3aba821 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Sep 2014 14:49:58 -0700
Subject: [PATCH] lifetime of expressions from model follow life-time of model,
 not the push/pop scope making scope based reference counting error prone

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f17f7a586..f0c31d800 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -60,6 +60,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_expr(r));
         Z3_CATCH_RETURN(0);
     }
@@ -263,6 +264,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_NON_NULL(f, 0);
         expr * e = to_func_interp_ref(f)->get_else();
+        mk_c(c)->save_ast_trail(e);
         RETURN_Z3(of_expr(e));
         Z3_CATCH_RETURN(0);
     }
@@ -301,6 +303,7 @@ extern "C" {
         LOG_Z3_func_entry_get_value(c, e);
         RESET_ERROR_CODE();
         expr * v = to_func_entry_ref(e)->get_result();
+        mk_c(c)->save_ast_trail(v);
         RETURN_Z3(of_expr(v));
         Z3_CATCH_RETURN(0);
     }