diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 86166a5cf..e7ae685fc 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -14,7 +14,7 @@ Author:
     Christoph M. Wintersteiger (cwinter) 2013-06-05
 
 Notes:
-    
+
 --*/
 #include<iostream>
 #include"z3.h"
@@ -27,21 +27,22 @@ extern "C" {
     Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_rounding_mode_sort(c);
-        RESET_ERROR_CODE(); 
-        api::context * ctx = mk_c(c);        
-        Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort());
-        RETURN_Z3(r);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        sort * s = ctx->fpautil().mk_rm_sort();
+        mk_c(c)->save_ast_trail(s);
+        RETURN_Z3(of_sort(s));
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c)
-    {
+    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -50,19 +51,20 @@ extern "C" {
         LOG_Z3_mk_fpa_rne(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c)
-    {
+    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_nearest_ties_to_away(c);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -71,19 +73,20 @@ extern "C" {
         LOG_Z3_mk_fpa_rna(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c)
-    {
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_toward_positive(c);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_positive();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -92,19 +95,20 @@ extern "C" {
         LOG_Z3_mk_fpa_rtp(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_positive();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)
-    {
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_toward_negative(c);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_negative();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -113,19 +117,20 @@ extern "C" {
         LOG_Z3_mk_fpa_rtn(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_negative();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c)
-    {
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_toward_zero(c);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_zero();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -134,8 +139,9 @@ extern "C" {
         LOG_Z3_mk_fpa_rtz(c);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_toward_zero();
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -143,13 +149,14 @@ extern "C" {
     Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) {
         Z3_TRY;
         LOG_Z3_mk_fpa_sort(c, ebits, sbits);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         if (ebits < 2 || sbits < 3) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-        }        
-        api::context * ctx = mk_c(c);        
-        Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits));
-        RETURN_Z3(r);
+        }
+        api::context * ctx = mk_c(c);
+        sort * s = ctx->fpautil().mk_float_sort(ebits, sbits);
+        ctx->save_ast_trail(s);
+        RETURN_Z3(of_sort(s));
         Z3_CATCH_RETURN(0);
     }
 
@@ -188,21 +195,23 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) {
         Z3_TRY;
         LOG_Z3_mk_fpa_nan(c, s);
-        RESET_ERROR_CODE();         
+        RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_nan(to_sort(s));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) {
         Z3_TRY;
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) : 
-                                          ctx->fpautil().mk_pinf(to_sort(s)));
-        RETURN_Z3(r);
+        expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
+                                   ctx->fpautil().mk_pinf(to_sort(s));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -211,9 +220,10 @@ extern "C" {
         LOG_Z3_mk_fpa_inf(c, s, negative);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) : 
-                                          ctx->fpautil().mk_pzero(to_sort(s)));
-        RETURN_Z3(r);
+        expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
+                                   ctx->fpautil().mk_pzero(to_sort(s));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -222,8 +232,9 @@ extern "C" {
         LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -233,12 +244,13 @@ extern "C" {
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
         scoped_mpf tmp(ctx->fpautil().fm());
-        ctx->fpautil().fm().set(tmp, 
-                                 ctx->fpautil().get_ebits(to_sort(ty)), 
-                                 ctx->fpautil().get_sbits(to_sort(ty)), 
-                                 v);
-        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
-        RETURN_Z3(r);
+        ctx->fpautil().fm().set(tmp,
+                                ctx->fpautil().get_ebits(to_sort(ty)),
+                                ctx->fpautil().get_sbits(to_sort(ty)),
+                                v);
+        expr * a = ctx->fpautil().mk_value(tmp);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -249,8 +261,9 @@ extern "C" {
         api::context * ctx = mk_c(c);
         scoped_mpf tmp(ctx->fpautil().fm());
         ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v);
-        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_value(tmp);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -261,11 +274,12 @@ extern "C" {
         api::context * ctx = mk_c(c);
         scoped_mpf tmp(ctx->fpautil().fm());
         ctx->fpautil().fm().set(tmp,
-                                   ctx->fpautil().get_ebits(to_sort(ty)),
-                                   ctx->fpautil().get_sbits(to_sort(ty)),
-                                   v);
-        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
-        RETURN_Z3(r);
+                                ctx->fpautil().get_ebits(to_sort(ty)),
+                                ctx->fpautil().get_sbits(to_sort(ty)),
+                                v);
+        expr * a = ctx->fpautil().mk_value(tmp);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -275,12 +289,13 @@ extern "C" {
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
         scoped_mpf tmp(ctx->fpautil().fm());
-        ctx->fpautil().fm().set(tmp, 
-                                   ctx->fpautil().get_ebits(to_sort(ty)), 
-                                   ctx->fpautil().get_sbits(to_sort(ty)), 
-                                   sgn != 0, sig, exp);
-        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
-        RETURN_Z3(r);
+        ctx->fpautil().fm().set(tmp,
+                                ctx->fpautil().get_ebits(to_sort(ty)),
+                                ctx->fpautil().get_sbits(to_sort(ty)),
+                                sgn != 0, sig, exp);
+        expr * a = ctx->fpautil().mk_value(tmp);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -291,111 +306,122 @@ extern "C" {
         api::context * ctx = mk_c(c);
         scoped_mpf tmp(ctx->fpautil().fm());
         ctx->fpautil().fm().set(tmp,
-                                   ctx->fpautil().get_ebits(to_sort(ty)),
-                                   ctx->fpautil().get_sbits(to_sort(ty)),
-                                   sgn != 0, sig, exp);
-        Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
-        RETURN_Z3(r);
+                                ctx->fpautil().get_ebits(to_sort(ty)),
+                                ctx->fpautil().get_sbits(to_sort(ty)),
+                                sgn != 0, sig, exp);
+        expr * a = ctx->fpautil().mk_value(tmp);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_abs(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_abs(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_neg(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_neg(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_add(c, rm, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
         Z3_TRY;
         LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_sqrt(c, rm, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_rem(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_round_to_integral(c, rm, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -404,8 +430,9 @@ extern "C" {
         LOG_Z3_mk_fpa_min(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -418,14 +445,15 @@ extern "C" {
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_leq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_le(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -434,18 +462,20 @@ extern "C" {
         LOG_Z3_mk_fpa_lt(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) {
         Z3_TRY;
         LOG_Z3_mk_fpa_geq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -454,8 +484,9 @@ extern "C" {
         LOG_Z3_mk_fpa_gt(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -464,18 +495,20 @@ extern "C" {
         LOG_Z3_mk_fpa_eq(c, t1, t2);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
-   
+
     Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_mk_fpa_is_normal(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_normal(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -484,8 +517,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_subnormal(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_subnormal(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -494,8 +528,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_zero(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_zero(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -504,8 +539,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_infinite(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_inf(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -514,8 +550,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_nan(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_nan(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -524,8 +561,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_negative(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_negative(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -534,8 +572,9 @@ extern "C" {
         LOG_Z3_mk_fpa_is_positive(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_is_positive(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -551,8 +590,9 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(bv)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -562,14 +602,15 @@ extern "C" {
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
         fpa_util & fu = ctx->fpautil();
-        if (!fu.is_rm(to_expr(rm)) || 
+        if (!fu.is_rm(to_expr(rm)) ||
             !fu.is_float(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -585,8 +626,9 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -602,8 +644,9 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -613,14 +656,15 @@ extern "C" {
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
         fpa_util & fu = ctx->fpautil();
-        if (!fu.is_rm(to_expr(rm)) || 
+        if (!fu.is_rm(to_expr(rm)) ||
             !ctx->bvutil().is_bv(to_expr(t)) ||
             !fu.is_float(to_sort(s))) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -629,8 +673,9 @@ extern "C" {
         LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -639,8 +684,9 @@ extern "C" {
         LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz);
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -649,8 +695,9 @@ extern "C" {
         LOG_Z3_mk_fpa_to_real(c, t);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
-        Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t)));
-        RETURN_Z3(r);
+        expr * a = ctx->fpautil().mk_to_real(to_expr(t));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }
 
@@ -689,7 +736,7 @@ extern "C" {
         return r;
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_get_numeral_significand_string(c, t);
@@ -699,14 +746,14 @@ extern "C" {
         unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
-        scoped_mpf val(mpfm);        
-        if (!plugin->is_numeral(to_expr(t), val)) {            
+        scoped_mpf val(mpfm);
+        if (!plugin->is_numeral(to_expr(t), val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
         else if (!mpfm.is_regular(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG)
-            return "";
+                return "";
         }
         unsigned sbits = val.get().get_sbits();
         scoped_mpq q(mpqm);
@@ -726,7 +773,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_exponent_string(c, t);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpautil().fm();        
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
@@ -738,7 +785,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG)
                 return "";
         }
-        mpf_exp_t exp = mpfm.exp_normalized(val);        
+        mpf_exp_t exp = mpfm.exp_normalized(val);
         std::stringstream ss;
         ss << exp;
         return mk_c(c)->mk_external_string(ss.str());
@@ -753,7 +800,7 @@ extern "C" {
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
-        bool r = plugin->is_numeral(to_expr(t), val);        
+        bool r = plugin->is_numeral(to_expr(t), val);
         if (!r) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
@@ -775,7 +822,7 @@ extern "C" {
 
     Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) {
         Z3_TRY;
-        LOG_Z3_mk_fpa_to_fp_int_real(c, rm, exp, sig, s);
+        LOG_Z3_mk_fpa_to_fp_int_real(c, rm, sig, exp, s);
         RESET_ERROR_CODE();
         api::context * ctx = mk_c(c);
         fpa_util & fu = ctx->fpautil();
@@ -786,8 +833,9 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp)));
-        RETURN_Z3(r);
+        expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp));
+        ctx->save_ast_trail(a);
+        RETURN_Z3(of_expr(a));
         Z3_CATCH_RETURN(0);
     }