diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index b0c7f7f58..9239eb255 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -71,6 +71,7 @@ VER_BUILD=None
 VER_REVISION=None
 PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0]
 GMP=False
+FOCI2=False
 VS_PAR=False
 VS_PAR_NUM=8
 GPROF=False
@@ -199,6 +200,14 @@ def test_gmp(cc):
     t.commit()
     return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
 
+def test_foci2(cc):
+    if is_verbose():
+        print("Testing FOCI2...")
+    t = TempFile('tstfoci2.cpp')
+    t.add('#include<foci2.h>\nint main() { mpz_t t; mpz_init(t); mpz_clear(t); return 0; }\n')
+    t.commit()
+    return exec_compiler_cmd([cc, CPPFLAGS, 'tstfoci2.cpp', LDFLAGS, '-lfoci2']) == 0
+
 def test_openmp(cc):
     if is_verbose():
         print("Testing OpenMP...")
@@ -444,6 +453,7 @@ def display_help(exit_code):
     if not IS_WINDOWS:
         print("  -g, --gmp                     use GMP.")
         print("  --gprof                       enable gprof")
+    print("  --foci2                       use FOCI2.")
     print("")
     print("Some influential environment variables:")
     if not IS_WINDOWS:
@@ -459,7 +469,7 @@ def display_help(exit_code):
 # Parse configuration option for mk_make script
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
-    global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
+    global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:], 
                                                'b:dsxhmcvtnp:gj', 
@@ -508,6 +518,8 @@ def parse_options():
             VS_PAR_NUM = int(arg)
         elif opt in ('-g', '--gmp'):
             GMP = True
+        elif opt in ('-f', '--foci2'):
+            FOCI2 = True
         elif opt in ('-j', '--java'):
             JAVA_ENABLED = True
         elif opt == '--gprof':
@@ -1458,7 +1470,7 @@ def mk_config():
                 print('JNI Bindings:   %s' % JNI_HOME)
                 print('Java Compiler:  %s' % JAVAC)
     else:
-        global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS
+        global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS
         ARITH = "internal"
         check_ar()
         CXX = find_cxx_compiler()
@@ -1475,6 +1487,12 @@ def mk_config():
             SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
         else:
             CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
+        if FOCI2:
+            test_foci2(CXX)
+            LDFLAGS  = '%s -lfoci2' % LDFLAGS
+            SLIBEXTRAFLAGS = '%s -lfoci2' % SLIBEXTRAFLAGS
+        else:
+            CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
         if GIT_HASH:
             CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
         CXXFLAGS = '%s -c' % CXXFLAGS
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 246d5cd8c..75adbb7d7 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -90,7 +90,7 @@ extern "C" {
 	
 	ptr_vector<ast> interpolants(num-1); // make space for result
 	
-	scoped_ptr<ast_manager> _m(&mk_c(ctx)->m());
+	ast_manager &_m = mk_c(ctx)->m();
 	iz3interpolate(_m,
 		       to_ast(proof),
 		       pre_cnsts_vec,
@@ -100,10 +100,12 @@ extern "C" {
 		       0); // ignore params for now FIXME
 
 	// copy result back
-	for(unsigned i = 0; i < interpolants.size(); i++)
+	for(unsigned i = 0; i < interpolants.size(); i++){
+	  mk_c(ctx)->save_ast_trail(interpolants[i]);
 	  interps[i] = of_ast(interpolants[i]);
+	  _m.dec_ref(interpolants[i]);
+	}
       }
-
   }
 
   Z3_lbool Z3_interpolate(Z3_context ctx,
@@ -120,6 +122,8 @@ extern "C" {
 			  ){
 
     
+    profiling::timer_start("Solve");
+
     if(!incremental){
 
       profiling::timer_start("Z3 assert");
@@ -159,6 +163,10 @@ extern "C" {
 			   interps,
 			   num_theory,
 			   theory);
+
+      if(!incremental)
+	for(int i = 0; i < num-1; i++)
+	  Z3_persist_ast(ctx,interps[i],1);
       break;
       
     case Z3_L_UNDEF:
@@ -172,6 +180,13 @@ extern "C" {
       break;
     }
 
+    profiling::timer_start("Z3 pop");
+    if(!incremental)
+      Z3_pop(ctx,1);
+    profiling::timer_stop("Z3 pop");
+
+    profiling::timer_stop("Solve");
+
     return result;
 
   }
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 296688086..51bf59798 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -140,7 +140,7 @@ iz3base::ast iz3base::simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<as
   ast not_lit = mk_not(lit);
   if(n == not_lit) return mk_false();
   if(op(n) != And || depth <= 0) return n;
-  std::pair<ast,ast> foo(n,(ast)0);
+  std::pair<ast,ast> foo(n,ast());
   std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
   ast &res = bar.first->second;
   if(!bar.second) return res;
@@ -159,7 +159,7 @@ iz3base::ast iz3base::simplify_with_lit(ast n, ast lit){
 
 iz3base::ast iz3base::simplify(ast n){
   if(is_not(n)) return mk_not(simplify(mk_not(n)));
-  std::pair<ast,ast> memo_obj(n,(ast)0);
+  std::pair<ast,ast> memo_obj(n,ast());
   std::pair<hash_map<ast,ast>::iterator,bool> memo = simplify_memo.insert(memo_obj);
   ast &res = memo.first->second;
   if(!memo.second) return res;
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index 8a8ad332a..b379be30c 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -56,7 +56,7 @@ class iz3base : public iz3mgr, public scopes {
 
   /** Constructor */
 
-  iz3base(scoped_ptr<ast_manager> &_m_manager,
+  iz3base(ast_manager &_m_manager,
 	 const std::vector<ast> &_cnsts,
 	 const std::vector<int> &_parents,
 	 const std::vector<ast> &_theory)
diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index 0317a9834..53e4ec84b 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -197,7 +197,7 @@ public:
 
   // convert an expr to Z3 ast
   ast to_Z3_ast(foci2::ast i){
-    std::pair<foci2::ast,ast> foo(i,(ast)0);
+    std::pair<foci2::ast,ast> foo(i,ast());
     std::pair<NodeToAst::iterator,bool> bar = node_to_ast.insert(foo);
     if(!bar.second) return bar.first->second;
     ast &res = bar.first->second;
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 0289c90c7..6da83004d 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -224,11 +224,11 @@ public:
     delete sp;
   }
 
-  iz3interp(scoped_ptr<ast_manager> &_m_manager)
+  iz3interp(ast_manager &_m_manager)
     : iz3mgr(_m_manager) {}
 };
 
-void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
+void iz3interpolate(ast_manager &_m_manager,
 		    ast *proof,
 		    const ptr_vector<ast> &cnsts,
 		    const ::vector<int> &parents,
@@ -236,21 +236,21 @@ void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
 		    const ptr_vector<ast> &theory,
 		    interpolation_options_struct * options)
 {
-  std::vector<ast_r> _cnsts(cnsts.size());
+  iz3interp itp(_m_manager);
+  std::vector<iz3mgr::ast> _cnsts(cnsts.size());
   std::vector<int> _parents(parents.size());
-  std::vector<ast_r> _interps;
-  std::vector<ast_r> _theory(theory.size());
+  std::vector<iz3mgr::ast> _interps;
+  std::vector<iz3mgr::ast> _theory(theory.size());
   for(unsigned i = 0; i < cnsts.size(); i++)
-    _cnsts[i] = cnsts[i];
+    _cnsts[i] = itp.cook(cnsts[i]);
   for(unsigned i = 0; i < parents.size(); i++)
     _parents[i] = parents[i];
   for(unsigned i = 0; i < theory.size(); i++)
-    _theory[i] = theory[i];
-  ast_r _proof(proof);
-  iz3interp itp(_m_manager);
+    _theory[i] = itp.cook(theory[i]);
+  iz3mgr::ast _proof = itp.cook(proof);
   itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options);
   interps.resize(_interps.size());
   for(unsigned i = 0; i < interps.size(); i++)
-    _interps[i] = interps[i];
+    interps[i] = itp.uncook(_interps[i]);
 }
 
diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h
index 65ba1f15a..d87aefba8 100644
--- a/src/interp/iz3interp.h
+++ b/src/interp/iz3interp.h
@@ -29,7 +29,7 @@ struct interpolation_options_struct {
 
 typedef interpolation_options_struct *interpolation_options;
 
-void iz3interpolate(scoped_ptr<ast_manager> &_m_manager,
+void iz3interpolate(ast_manager &_m_manager,
 		    ast *proof,
 		    const ptr_vector<ast> &cnsts,
 		    const ::vector<int> &parents,
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index 93f541430..fd9b17edc 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -40,7 +40,7 @@ std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){
 
 iz3mgr::ast iz3mgr::make_var(const std::string &name, type ty){ 
   symbol s = symbol(name.c_str());
-  return m().mk_const(m().mk_const_decl(s, ty));
+  return cook(m().mk_const(m().mk_const_decl(s, ty)));
 }
 
 iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
@@ -91,7 +91,7 @@ iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
 }
 
 iz3mgr::ast iz3mgr::mki(family_id fid, decl_kind dk, int n, raw_ast **args){
-  return m().mk_app(fid, dk, 0, 0, n, (expr **)args);        
+  return cook(m().mk_app(fid, dk, 0, 0, n, (expr **)args));        
 }
 
 iz3mgr::ast iz3mgr::make(opr op, const std::vector<ast> &args){
@@ -128,7 +128,7 @@ iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1, ast &arg2){
 }
 
 iz3mgr::ast iz3mgr::make(symb sym, int n, raw_ast **args){
-  return m().mk_app(sym, n, (expr **) args);   
+  return cook(m().mk_app(sym, n, (expr **) args));   
 }
 
 iz3mgr::ast iz3mgr::make(symb sym, const std::vector<ast> &args){
@@ -193,14 +193,16 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
 			     0, 0,
 			     0, 0
 			     );
-  return result.get();
+  return cook(result.get());
 }
 
+// FIXME replace this with existing Z3 functionality
+
 iz3mgr::ast iz3mgr::clone(ast &t, const std::vector<ast> &_args){
   if(_args.size() == 0)
     return t;
 
-  ast_manager& m = *m_manager.get();
+  ast_manager& m = m_manager;
   expr* a = to_expr(t.raw());
   static std::vector<raw_ast*> rargs(10);
   if(rargs.size() < _args.size())
@@ -231,7 +233,7 @@ iz3mgr::ast iz3mgr::clone(ast &t, const std::vector<ast> &_args){
   default:
     break;
   }            
-  return a;
+  return cook(a);
 }
 
 
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index c96a20c7b..4f247bb81 100644
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -53,32 +53,65 @@ Revision History:
 typedef ast raw_ast;
 
 /** Wrapper around an ast pointer */
-class ast_r {
+class ast_i {
+ protected:
   raw_ast *_ast;
  public:
   raw_ast * const &raw() const {return _ast;}
-  ast_r(raw_ast *a){_ast = a;}
+  ast_i(raw_ast *a){_ast = a;}
   
-  ast_r(){_ast = 0;}
-  bool eq(const ast_r &other) const {
+  ast_i(){_ast = 0;}
+  bool eq(const ast_i &other) const {
     return _ast == other._ast;
   }
-  bool lt(const ast_r &other) const {
+  bool lt(const ast_i &other) const {
     return _ast < other._ast;
   }
-  friend bool operator==(const ast_r &x, const ast_r&y){
+  friend bool operator==(const ast_i &x, const ast_i&y){
     return x.eq(y);
   }
-  friend bool operator!=(const ast_r &x, const ast_r&y){
+  friend bool operator!=(const ast_i &x, const ast_i&y){
     return !x.eq(y);
   }
-  friend bool operator<(const ast_r &x, const ast_r&y){
+  friend bool operator<(const ast_i &x, const ast_i&y){
     return x.lt(y);
   }
   size_t hash() const {return (size_t)_ast;}
   bool null() const {return !_ast;}
 };
 
+/** Reference counting verison of above */
+class ast_r : public ast_i {
+  ast_manager *_m;
+ public:
+  ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
+    _m = m;
+    m->inc_ref(a);
+  }
+  
+  ast_r() {_m = 0;}
+
+  ast_r(const ast_r &other) : ast_i(other) {
+    _m = other._m;
+    _m->inc_ref(_ast);
+  }
+
+  ast_r &operator=(const ast_r &other) {
+    if(_ast)
+      _m->dec_ref(_ast);
+    _ast = other._ast;
+    _m = other._m;
+    _m->inc_ref(_ast);
+    return *this;
+  }
+
+  ~ast_r(){
+    if(_ast)
+      _m->dec_ref(_ast);
+  }
+  
+
+};
 
 // to make ast_r hashable
 namespace stl_ext {
@@ -186,8 +219,14 @@ class iz3mgr  {
   ast make_quant(opr op, const std::vector<ast> &bvs, ast &body);
   ast clone(ast &t, const std::vector<ast> &args);
 
-  ast_manager &m() {return *m_manager.get();}
+  ast_manager &m() {return m_manager;}
 
+  ast cook(raw_ast *a) {return ast(&m_manager,a);}
+
+  raw_ast *uncook(const ast &a) {
+    m_manager.inc_ref(a.raw());
+    return a.raw();
+  }
 
   /** Methods for destructing ast. */
 
@@ -210,13 +249,13 @@ class iz3mgr  {
     ast_kind dk = t.raw()->get_kind();
     switch(dk){
     case AST_APP:
-      return to_app(t.raw())->get_arg(i);
+      return cook(to_app(t.raw())->get_arg(i));
     case AST_QUANTIFIER:
-      return to_quantifier(t.raw())->get_expr();
+      return cook(to_quantifier(t.raw())->get_expr());
     default:;
     }
     assert(0);
-    return ast((raw_ast *)0);
+    return ast();
   }
   
   symb sym(ast t){
@@ -262,7 +301,7 @@ class iz3mgr  {
   }
 
   ast get_quantifier_body(const ast &t) {
-    return to_quantifier(t.raw())->get_expr();
+    return cook(to_quantifier(t.raw())->get_expr());
   }
 
   unsigned get_variable_index_value(const ast &t) {
@@ -359,7 +398,7 @@ class iz3mgr  {
 
   ast make_int(const std::string &s) {
     sort *r = m().mk_sort(m_arith_fid, INT_SORT);
-    return m_arith_util.mk_numeral(rational(s.c_str()),r);
+    return cook(m_arith_util.mk_numeral(rational(s.c_str()),r));
   }
 
 
@@ -392,9 +431,9 @@ class iz3mgr  {
 
   static void pretty_print(std::ostream &f, const std::string &s);
 
-  iz3mgr(scoped_ptr<ast_manager> &_m_manager)
+  iz3mgr(ast_manager &_m_manager)
     : m_manager(_m_manager),
-    m_arith_util(*_m_manager)
+    m_arith_util(_m_manager)
     {
       m_basic_fid = m().get_basic_family_id();
       m_arith_fid = m().mk_family_id("arith");
@@ -406,7 +445,7 @@ class iz3mgr  {
   
  iz3mgr(const iz3mgr& other)
    : m_manager(other.m_manager),
-    m_arith_util((const arith_util&)*other.m_manager)
+    m_arith_util(other.m_manager)
   {
       m_basic_fid = m().get_basic_family_id();
       m_arith_fid = m().mk_family_id("arith");
@@ -417,7 +456,7 @@ class iz3mgr  {
   }
 
  protected:
-  scoped_ptr<ast_manager> m_manager;
+  ast_manager &m_manager;
 
  private:
   ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index 0500d88ab..a16d079c8 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -625,7 +625,7 @@ public:
   ast cont_eq(bool truth, ast v, ast e){
     if(is_not(e)) return cont_eq(!truth,v,arg(e,0));
     if(cont_eq_memo.find(e) != cont_eq_memo.end())
-      return (ast)0;
+      return ast();
     cont_eq_memo.insert(e);
     if(!truth && op(e) == Equal){
       if(arg(e,0) == v) return(arg(e,1));
@@ -645,7 +645,7 @@ public:
   
   ast subst(ast var, ast t, ast e){
     if(e == var) return t;
-    std::pair<ast,ast> foo(e,(ast)0);
+    std::pair<ast,ast> foo(e,ast());
     std::pair<AstToAst::iterator,bool> bar = subst_memo.insert(foo);
     ast &res = bar.first->second;
     if(bar.second){
@@ -1722,7 +1722,7 @@ public:
     for(unsigned i = 0; i < theory.size(); i++)
       frame_map[theory[i]] = INT_MAX;
     frames = cnsts.size();
-    traced_lit = 0;
+    traced_lit = ast();
   }
 };