diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp
index 99a538549..fa7d8b896 100755
--- a/examples/interp/iz3.cpp
+++ b/examples/interp/iz3.cpp
@@ -32,6 +32,7 @@ int main(int argc, const char **argv) {
   std::string output_file;
   bool flat_mode = false;
   bool anonymize = false;
+  bool write = false;
 
   Z3_config cfg = Z3_mk_config();
   // Z3_interpolation_options options = Z3_mk_interpolation_options();
@@ -65,6 +66,8 @@ int main(int argc, const char **argv) {
         flat_mode = true;
       else if(flag == "-a" || flag == "--anon")
         anonymize = true;
+      else if(flag == "-w" || flag == "--write")
+        write = true;
       else if(flag == "-s" || flag == "--simple")
         Z3_set_param_value(cfg,"PREPROCESS","false");
       else
@@ -80,7 +83,9 @@ int main(int argc, const char **argv) {
   /* Create a Z3 context to contain formulas */
   Z3_context ctx = Z3_mk_interpolation_context(cfg);
 
-  if(!flat_mode)
+  if(write || anonymize)
+    Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);
+  else if(!flat_mode)
     Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT);
   
   /* Read an interpolation problem */
@@ -119,17 +124,17 @@ int main(int argc, const char **argv) {
     }
   }
 
-#if 0
   /* Write out anonymized version. */
 
-  if(anonymize){
+  if(write || anonymize){
+#if 0
     Z3_anonymize_ast_vector(ctx,num,constraints);
-    std::string ofn = output_file.empty() ? "anon.smt" : output_file;
-    Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str());
+#endif
+    std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file;
+    Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory,  theory);
     std::cout << "anonymized problem written to " << ofn << "\n";
     exit(0);
   }
-#endif
 
   /* Compute an interpolant, or get a model. */
 
@@ -188,7 +193,7 @@ int main(int argc, const char **argv) {
       printf("interpolant written to %s\n",output_file.c_str());
 #endif
     }
-#if 0
+#if 1
     if(check_mode){
       std::cout << "Checking interpolant...\n";
       bool chk;
@@ -212,6 +217,7 @@ int main(int argc, const char **argv) {
     break;
   }
 
+  if(profile_mode)
     std::cout << Z3_interpolation_profile(ctx);
 
   /* Delete the model if there is one */
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index f5156ede6..f23c4fe80 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -33,7 +33,8 @@ def init_project_def():
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('solver', ['model', 'tactic'])
-    add_lib('cmd_context', ['solver', 'rewriter'])
+    add_lib('interp', ['solver'])
+    add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
     add_lib('proof_checker', ['rewriter'], 'ast/proof_checker')
@@ -59,10 +60,10 @@ def init_project_def():
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
-    add_dll('foci2', ['util'], 'interp/foci2stub', 
-            dll_name='foci2', 
-            export_files=['foci2stub.cpp'])
-    add_lib('interp', ['solver','foci2'])
+#    add_dll('foci2', ['util'], 'interp/foci2stub', 
+#            dll_name='foci2', 
+#            export_files=['foci2stub.cpp'])
+#    add_lib('interp', ['solver','foci2'])
     API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
     add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp'],
             includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 9239eb255..c2a168b70 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -72,6 +72,7 @@ VER_REVISION=None
 PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0]
 GMP=False
 FOCI2=False
+FOCI2LIB=''
 VS_PAR=False
 VS_PAR_NUM=8
 GPROF=False
@@ -200,13 +201,13 @@ def test_gmp(cc):
     t.commit()
     return exec_compiler_cmd([cc, CPPFLAGS, 'tstgmp.cpp', LDFLAGS, '-lgmp']) == 0
 
-def test_foci2(cc):
+def test_foci2(cc,foci2lib):
     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.add('#include<foci2.h>\nint main() { foci2 *f = foci2::create("lia"); return 0; }\n')
     t.commit()
-    return exec_compiler_cmd([cc, CPPFLAGS, 'tstfoci2.cpp', LDFLAGS, '-lfoci2']) == 0
+    return exec_compiler_cmd([cc, CPPFLAGS, '-Isrc/interp', 'tstfoci2.cpp', LDFLAGS, foci2lib]) == 0
 
 def test_openmp(cc):
     if is_verbose():
@@ -453,7 +454,7 @@ def display_help(exit_code):
     if not IS_WINDOWS:
         print("  -g, --gmp                     use GMP.")
         print("  --gprof                       enable gprof")
-    print("  --foci2                       use FOCI2.")
+    print("  -f <path> --foci2=<path>          use foci2 library at path")
     print("")
     print("Some influential environment variables:")
     if not IS_WINDOWS:
@@ -469,18 +470,19 @@ 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, FOCI2, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
+    global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:], 
-                                               'b:dsxhmcvtnp:gj', 
+                                               'b:df:sxhmcvtnp:gj', 
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
-                                                'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof',
+                                                'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
                                                 'githash='])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
 
     for opt, arg in options:
+        print('opt = %s, arg = %s' % (opt, arg))
         if opt in ('-b', '--build'):
             if arg == 'src':
                 raise MKException('The src directory should not be used to host the Makefile')
@@ -520,6 +522,7 @@ def parse_options():
             GMP = True
         elif opt in ('-f', '--foci2'):
             FOCI2 = True
+            FOCI2LIB = arg
         elif opt in ('-j', '--java'):
             JAVA_ENABLED = True
         elif opt == '--gprof':
@@ -1470,7 +1473,7 @@ def mk_config():
                 print('JNI Bindings:   %s' % JNI_HOME)
                 print('Java Compiler:  %s' % JAVAC)
     else:
-        global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS
+        global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
         ARITH = "internal"
         check_ar()
         CXX = find_cxx_compiler()
@@ -1488,11 +1491,12 @@ def mk_config():
         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 test_foci2(CXX,FOCI2LIB):
+                LDFLAGS  = '%s %s' % (LDFLAGS,FOCI2LIB)
+                SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
+            else:
+                print "FAILED\n"
+                FOCI2 = False
         if GIT_HASH:
             CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
         CXXFLAGS = '%s -c' % CXXFLAGS
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index e93e1a178..5e8b2b861 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -208,6 +208,7 @@ extern "C" {
     MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP);
     MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP);
     MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP);
+    MK_UNARY(Z3_mk_interp, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP);
 
     Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
         expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));
@@ -927,6 +928,7 @@ extern "C" {
             case OP_NOT:      return Z3_OP_NOT;
             case OP_IMPLIES:  return Z3_OP_IMPLIES;
             case OP_OEQ:      return Z3_OP_OEQ;
+            case OP_INTERP:   return Z3_OP_INTERP;
 
             case PR_UNDEF:    return Z3_OP_PR_UNDEF;
             case PR_TRUE:     return Z3_OP_PR_TRUE;
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 75adbb7d7..926493c6b 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -16,6 +16,7 @@ Revision History:
 
 --*/
 #include<iostream>
+#include<sstream>
 #include"z3.h"
 #include"api_log_macros.h"
 #include"api_context.h"
@@ -34,6 +35,8 @@ Revision History:
 #include"iz3interp.h"
 #include"iz3profiling.h"
 #include"iz3hash.h"
+#include"iz3pp.h"
+#include"iz3checker.h"
 
 #ifndef WIN32
 using namespace stl_ext;
@@ -47,8 +50,8 @@ extern "C" {
     if(!cfg) cfg = Z3_mk_config();
     Z3_set_param_value(cfg, "PROOF", "true");
     Z3_set_param_value(cfg, "MODEL", "true");
-    Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false");
-    Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
+    // Z3_set_param_value(cfg, "PRE_SIMPLIFIER","false");
+    // Z3_set_param_value(cfg, "SIMPLIFY_CLAUSES","false");
     
     Z3_context ctx = Z3_mk_context(cfg);
     Z3_del_config(cfg);
@@ -191,6 +194,64 @@ extern "C" {
 
   }
   
+  static std::ostringstream itp_err;
+
+  int Z3_check_interpolant(Z3_context ctx, 
+			    int num, 
+			    Z3_ast *cnsts, 
+			    int *parents,
+			    Z3_ast *itp,
+			    const char **error,
+			    int num_theory,
+			    Z3_ast *theory){
+
+    ast_manager &_m = mk_c(ctx)->m();
+    itp_err.clear();
+    
+    // need a solver -- make one here, but how?
+    params_ref p = params_ref::get_empty(); //FIXME
+    scoped_ptr<solver_factory> sf(mk_smt_solver_factory());
+    scoped_ptr<solver> sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA")));
+    
+    ptr_vector<ast> cnsts_vec(num);  // get constraints in a vector
+    for(int i = 0; i < num; i++){
+      ast *a = to_ast(cnsts[i]);
+      cnsts_vec[i] = a;
+    }
+    
+    ptr_vector<ast> itp_vec(num);  // get interpolants in a vector
+    for(int i = 0; i < num-1; i++){
+      ast *a = to_ast(itp[i]);
+      itp_vec[i] = a;
+    }
+
+    ::vector<int> parents_vec;  // get parents in a vector
+    if(parents){
+      parents_vec.resize(num);
+      for(int i = 0; i < num; i++)
+	parents_vec[i] = parents[i];
+    }
+    
+    ptr_vector<ast> theory_vec; // get background theory in a vector
+    if(theory){
+      theory_vec.resize(num_theory);
+      for(int i = 0; i < num_theory; i++)
+	theory_vec[i] = to_ast(theory[i]);
+    }
+    
+    bool res = iz3check(_m,
+			sp.get(),
+			itp_err,
+			cnsts_vec,
+			parents_vec,
+			itp_vec,
+			theory_vec);
+
+    *error = res ? 0 : itp_err.str().c_str();
+    return res;
+  }
+
+
   static std::string Z3_profile_string;
   
   Z3_string Z3_interpolation_profile(Z3_context ctx){
@@ -258,6 +319,7 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
 
 extern "C" {
 
+#if 0
   static void iZ3_write_seq(Z3_context ctx, int num, Z3_ast *cnsts, const char *filename, int num_theory, Z3_ast *theory){
     int num_fmlas = num+num_theory;
     std::vector<Z3_ast> fmlas(num_fmlas);
@@ -298,6 +360,89 @@ extern "C" {
     }
     iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory);
   }
+#else
+
+
+  static Z3_ast and_vec(Z3_context ctx,std::vector<Z3_ast> &c){
+    return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
+  }
+  
+  static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){
+    Z3_ast res;
+    if(!parents){
+      res = Z3_mk_interp(ctx,cnsts[0]);
+      for(int i = 1; i < num-1; i++){
+	Z3_ast bar[2] = {res,cnsts[i]};
+	res = Z3_mk_interp(ctx,Z3_mk_and(ctx,2,bar));
+      }
+      if(num > 1){
+	Z3_ast bar[2] = {res,cnsts[num-1]};
+	res = Z3_mk_and(ctx,2,bar);
+      }
+    }
+    else {
+      std::vector<std::vector<Z3_ast> > chs(num);
+      for(int i = 0; i < num-1; i++){
+	std::vector<Z3_ast> &c = chs[i];
+	c.push_back(cnsts[i]);
+	Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c));
+	chs[parents[i]].push_back(foo);
+      }
+      {
+	std::vector<Z3_ast> &c = chs[num-1];
+	c.push_back(cnsts[num-1]);
+	res = and_vec(ctx,c);
+      }
+    }
+    Z3_inc_ref(ctx,res);
+    return res;
+  }
+
+  void Z3_write_interpolation_problem(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, const char *filename, int num_theory, Z3_ast *theory){
+    std::ofstream f(filename);
+    if(num >  0){
+      ptr_vector<expr> cnsts_vec(num);  // get constraints in a vector
+      for(int i = 0; i < num; i++){
+	expr *a = to_expr(cnsts[i]);
+	cnsts_vec[i] = a;
+      }
+      Z3_ast tree = parents_vector_to_tree(ctx,num,cnsts,parents);
+      iz3pp(mk_c(ctx)->m(),cnsts_vec,to_expr(tree),f);
+      Z3_dec_ref(ctx,tree);
+    }
+    f.close();
+
+#if 0    
+
+    
+    if(!parents){
+      iZ3_write_seq(ctx,num,cnsts,filename,num_theory,theory);
+      return;
+    }
+    std::vector<Z3_ast> tcnsts(num);
+    hash_map<int,Z3_ast> syms;
+    for(int j = 0; j < num - 1; j++){
+      std::ostringstream oss;
+      oss << "$P" << j;
+      std::string name = oss.str();
+      Z3_symbol s = Z3_mk_string_symbol(ctx, name.c_str());
+      Z3_ast symbol = Z3_mk_const(ctx, s, Z3_mk_bool_sort(ctx));
+      syms[j] = symbol;
+      tcnsts[j] = Z3_mk_implies(ctx,cnsts[j],symbol);
+    }
+    tcnsts[num-1] = Z3_mk_implies(ctx,cnsts[num-1],Z3_mk_false(ctx));
+    for(int j = num-2; j >= 0; j--){
+      int parent = parents[j];
+      // assert(parent >= 0 && parent < num);
+      tcnsts[parent] = Z3_mk_implies(ctx,syms[j],tcnsts[parent]);
+    }
+    iZ3_write_seq(ctx,num,&tcnsts[0],filename,num_theory,theory);
+#endif
+
+  }
+
+
+#endif
 
   static std::vector<Z3_ast> read_cnsts;
   static std::vector<int> read_parents;
@@ -309,7 +454,7 @@ extern "C" {
     read_error.clear();
     try {
       std::string foo(filename);
-      if(!foo.empty() && foo[foo.size()-1] == '2'){
+      if(foo.size() >= 5 && foo.substr(foo.size()-5) == ".smt2"){
 	Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
 	Z3_app app = Z3_to_app(ctx,ass);
 	int nconjs = Z3_get_app_num_args(ctx,app);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 76c34121f..a64f1473d 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -249,6 +249,8 @@ typedef enum
    - Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms.
         It captures equisatisfiability and equivalence modulo renamings.
 
+   - Z3_OP_INTERP Marks a sub-formula for interpolation.
+
    - Z3_OP_ANUM Arithmetic numeral.
 
    - Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
@@ -890,6 +892,7 @@ typedef enum {
     Z3_OP_NOT,
     Z3_OP_IMPLIES,
     Z3_OP_OEQ,
+    Z3_OP_INTERP,
 
     // Arithmetic
     Z3_OP_ANUM = 0x200,
@@ -2102,6 +2105,16 @@ END_MLAPI_EXCLUDE
     */
     Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a);
     
+    /**
+        \brief \mlh mk_interp c a \endmlh 
+        Create an AST node marking a formula position for interpolation.
+        
+        The node \c a must have Boolean sort.
+
+        def_API('Z3_mk_interp', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_interp(__in Z3_context c, __in Z3_ast a);
+    
     /**
        \brief \mlh mk_ite c t1 t2 t2 \endmlh 
        Create an AST node representing an if-then-else: <tt>ite(t1, t2,
@@ -7807,6 +7820,7 @@ END_MLAPI_EXCLUDE
      valuation of the vertices that makes all the implications true
      where each value is represented using the common symbols between
      the formulas in the subtree and the remainder of the formulas.
+
   */
   
 
@@ -7822,6 +7836,51 @@ END_MLAPI_EXCLUDE
 
 
 
+  /** Check the correctness of an interpolant. The Z3 context must
+      have no constraints asserted when this call is made. That means
+      that after interpolating, you must first fully pop the Z3
+      context before calling this. See Z3_interpolate for meaning of parameters.
+
+      \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
+      \param num The number of constraints in the sequence
+      \param cnsts Array of constraints (AST's in context ctx)
+      \param parents The parents vector (or NULL for sequence)
+      \param interps The interpolant to check
+      \param error Returns an error message if interpolant incorrect (do not free the string)
+
+      Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
+      incorrect, and Z3_L_UNDEF if unknown.
+
+  */
+  
+  int Z3_API
+  Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
+                                       int num_theory, Z3_ast *theory);
+
+  /** Write an interpolation problem to file suitable for reading with
+      Z3_read_interpolation_problem. The output file is a sequence
+      of SMT-LIB2 format commands, suitable for reading with command-line Z3
+      or other interpolating solvers.
+
+      \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
+      \param num The number of constraints in the sequence
+      \param cnsts Array of constraints
+      \param parents The parents vector (or NULL for sequence)
+      \param filename The file name to write
+
+  */
+
+  void Z3_API
+  Z3_write_interpolation_problem(Z3_context ctx,
+				 int num, 
+				 Z3_ast *cnsts, 
+				 int *parents,
+				 const char *filename,
+                                 int num_theory,
+				 Z3_ast *theory);
+
+
+
 #endif
 
 
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 8d643a348..797e118a7 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -640,6 +640,7 @@ basic_decl_plugin::basic_decl_plugin():
     m_iff_decl(0),
     m_xor_decl(0),
     m_not_decl(0),
+    m_interp_decl(0),
     m_implies_decl(0),
     
     m_proof_sort(0),
@@ -863,6 +864,7 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_iff_decl     = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true);
     m_xor_decl     = mk_bool_op_decl("xor", OP_XOR, 2, true, true);
     m_not_decl     = mk_bool_op_decl("not", OP_NOT, 1);
+    m_interp_decl  = mk_bool_op_decl("interp", OP_INTERP, 1);
     m_implies_decl = mk_implies_decl();
     
     m_proof_sort = m->mk_sort(symbol("Proof"), sort_info(id, PROOF_SORT));
@@ -887,6 +889,7 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("or", OP_OR));
     op_names.push_back(builtin_name("xor", OP_XOR));
     op_names.push_back(builtin_name("not", OP_NOT));
+    op_names.push_back(builtin_name("interp", OP_INTERP));
     op_names.push_back(builtin_name("=>", OP_IMPLIES));
     if (logic == symbol::null) {
         // user friendly aliases
@@ -898,6 +901,7 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
         op_names.push_back(builtin_name("||", OP_OR));
         op_names.push_back(builtin_name("equals", OP_EQ));
         op_names.push_back(builtin_name("equiv", OP_IFF));
+        op_names.push_back(builtin_name("@@", OP_INTERP));
     }
 }
 
@@ -1016,6 +1020,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_AND:     return m_and_decl;
     case OP_OR:      return m_or_decl;
     case OP_NOT:     return m_not_decl;
+    case OP_INTERP:  return m_interp_decl;
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
@@ -1051,6 +1056,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_AND:     return m_and_decl;
     case OP_OR:      return m_or_decl;
     case OP_NOT:     return m_not_decl;
+    case OP_INTERP:  return m_interp_decl;
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 4c924691c..141c1c9a2 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1006,7 +1006,7 @@ enum basic_sort_kind {
 };
 
 enum basic_op_kind {
-    OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
+    OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP,
 
     PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
     PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT, 
@@ -1028,6 +1028,7 @@ protected:
     func_decl * m_iff_decl;
     func_decl * m_xor_decl;
     func_decl * m_not_decl;
+    func_decl * m_interp_decl;
     func_decl * m_implies_decl;
     ptr_vector<func_decl> m_eq_decls;  // cached eqs
     ptr_vector<func_decl> m_ite_decls; // cached ites
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 21a986fda..0e75a56ba 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -240,6 +240,8 @@ protected:
     symbol      m_produce_unsat_cores;
     symbol      m_produce_models;
     symbol      m_produce_assignments;
+    symbol      m_produce_interpolants;
+    symbol      m_check_interpolants;
     symbol      m_regular_output_channel;
     symbol      m_diagnostic_output_channel;
     symbol      m_random_seed;
@@ -253,7 +255,9 @@ protected:
         return 
             s == m_print_success || s == m_print_warning || s == m_expand_definitions || 
             s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores ||
-            s == m_produce_models || s == m_produce_assignments || s == m_regular_output_channel || s == m_diagnostic_output_channel || 
+            s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
+	    s == m_check_interpolants ||
+	    s == m_regular_output_channel || s == m_diagnostic_output_channel || 
             s == m_random_seed || s == m_verbosity || s == m_global_decls;
     }
 
@@ -270,6 +274,8 @@ public:
         m_produce_unsat_cores(":produce-unsat-cores"),
         m_produce_models(":produce-models"),
         m_produce_assignments(":produce-assignments"),
+        m_produce_interpolants(":produce-interpolants"),
+        m_check_interpolants(":check-interpolants"),
         m_regular_output_channel(":regular-output-channel"),
         m_diagnostic_output_channel(":diagnostic-output-channel"),
         m_random_seed(":random-seed"),
@@ -337,6 +343,13 @@ class set_option_cmd : public set_get_option_cmd {
             check_not_initialized(ctx, m_produce_proofs);
             ctx.set_produce_proofs(to_bool(value));
         }
+        else if (m_option == m_produce_interpolants) {
+            check_not_initialized(ctx, m_produce_interpolants);
+            ctx.set_produce_interpolants(to_bool(value));
+        }
+        else if (m_option == m_check_interpolants) {
+	    ctx.set_check_interpolants(to_bool(value));
+        }
         else if (m_option == m_produce_unsat_cores) {
             check_not_initialized(ctx, m_produce_unsat_cores);
             ctx.set_produce_unsat_cores(to_bool(value));
@@ -485,6 +498,9 @@ public:
         else if (opt == m_produce_proofs) {
             print_bool(ctx, ctx.produce_proofs());
         }
+        else if (opt == m_produce_interpolants) {
+            print_bool(ctx, ctx.produce_interpolants());
+        }
         else if (opt == m_produce_unsat_cores) {
             print_bool(ctx, ctx.produce_unsat_cores());
         }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 261af3092..f53c9850a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -38,6 +38,9 @@ Notes:
 #include"model_evaluator.h"
 #include"for_each_expr.h"
 #include"scoped_timer.h"
+#include"interpolant_cmds.h"
+//FIXME Does this break modularity?
+// #include"smt_solver.h"
 
 func_decls::func_decls(ast_manager & m, func_decl * f):
     m_decls(TAG(func_decl*, f, 0)) {
@@ -323,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     install_basic_cmds(*this);
     install_ext_basic_cmds(*this);
     install_core_tactic_cmds(*this);
+    install_interpolant_cmds(*this);
     SASSERT(m != 0 || !has_manager());
     if (m)
         init_external_manager();
@@ -380,6 +384,19 @@ void cmd_context::set_produce_proofs(bool f) {
     m_params.m_proof = f;
 }
 
+void cmd_context::set_produce_interpolants(bool f) {
+    // can only be set before initialization
+    // FIXME currently synonym for produce_proofs
+    // also sets the default solver to be simple smt
+    SASSERT(!has_manager());
+    m_params.m_proof = f;
+    // set_solver_factory(mk_smt_solver_factory());
+}
+
+void cmd_context::set_check_interpolants(bool f) {
+    m_params.m_check_interpolants = f;
+}
+
 bool cmd_context::produce_models() const { 
     return m_params.m_model;
 }
@@ -388,6 +405,15 @@ bool cmd_context::produce_proofs() const {
     return m_params.m_proof;
 }
 
+bool cmd_context::produce_interpolants() const { 
+    // FIXME currently synonym for produce_proofs
+    return m_params.m_proof;
+}
+
+bool cmd_context::check_interpolants() const { 
+    return m_params.m_check_interpolants;
+}
+
 bool cmd_context::produce_unsat_cores() const { 
     return m_params.m_unsat_core;
 }
@@ -1456,11 +1482,27 @@ void cmd_context::validate_model() {
     }
 }
 
+// FIXME: really interpolants_enabled ought to be a parameter to the solver factory,
+// but this is a global change, so for now, we use an alternate solver factory
+// for interpolation
+
 void cmd_context::mk_solver() {
     bool proofs_enabled, models_enabled, unsat_core_enabled;
     params_ref p;
     m_params.get_solver_params(m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
-    m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
+    if(produce_interpolants()){
+        SASSERT(m_interpolating_solver_factory);
+        m_solver = (*m_interpolating_solver_factory)(m(), p, true /* must have proofs */, models_enabled, unsat_core_enabled, m_logic);
+    }
+    else
+        m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
+}
+
+
+
+void cmd_context::set_interpolating_solver_factory(solver_factory * f) {
+  SASSERT(!has_manager());
+  m_interpolating_solver_factory   = f;
 }
 
 void cmd_context::set_solver_factory(solver_factory * f) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 22b2ea046..eac9a39ce 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -186,6 +186,7 @@ protected:
 
     svector<scope>               m_scopes;
     scoped_ptr<solver_factory>   m_solver_factory;
+    scoped_ptr<solver_factory>   m_interpolating_solver_factory;
     ref<solver>                  m_solver;
     ref<check_sat_result>        m_check_sat_result;
 
@@ -253,6 +254,7 @@ public:
     void cancel() { set_cancel(true); }
     void reset_cancel() { set_cancel(false); }
     context_params  & params() { return m_params; }
+    solver_factory &get_solver_factory() { return *m_solver_factory; }
     void global_params_updated(); // this method should be invoked when global (and module) params are updated.
     bool set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
@@ -275,12 +277,16 @@ public:
     void set_random_seed(unsigned s) { m_random_seed = s; }
     bool produce_models() const;
     bool produce_proofs() const;
+    bool produce_interpolants() const;
+    bool check_interpolants() const;
     bool produce_unsat_cores() const;
     bool well_sorted_check_enabled() const;
     bool validate_model_enabled() const;
     void set_produce_models(bool flag);
     void set_produce_unsat_cores(bool flag);
     void set_produce_proofs(bool flag);
+    void set_produce_interpolants(bool flag);
+    void set_check_interpolants(bool flag);
     bool produce_assignments() const { return m_produce_assignments; }
     void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
     void set_status(status st) { m_status = st; }
@@ -294,6 +300,7 @@ public:
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
  
     void set_solver_factory(solver_factory * s);
+    void set_interpolating_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index 2752967dd..0ec44e0cf 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -61,6 +61,9 @@ void context_params::set(char const * param, char const * value) {
     else if (p == "proof") {
         set_bool(m_proof, param, value);
     }
+    else if (p == "check_interpolants") {
+        set_bool(m_check_interpolants, param, value);
+    }
     else if (p == "model") {
         set_bool(m_model, param, value);
     }
@@ -96,6 +99,7 @@ void context_params::updt_params(params_ref const & p) {
     m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
     m_auto_config       = p.get_bool("auto_config", true);
     m_proof             = p.get_bool("proof", false);
+    m_check_interpolants = p.get_bool("check_interpolants", false);
     m_model             = p.get_bool("model", true);
     m_model_validate    = p.get_bool("model_validate", false);
     m_trace             = p.get_bool("trace", false);
@@ -111,6 +115,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
     d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
     d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
+    d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false");
     d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
     d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
     d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h
index 526b4f517..7271bb84f 100644
--- a/src/cmd_context/context_params.h
+++ b/src/cmd_context/context_params.h
@@ -29,6 +29,8 @@ class context_params {
 public:
     bool        m_auto_config;
     bool        m_proof;
+    bool        m_interpolants;
+    bool        m_check_interpolants;
     bool        m_debug_ref_count;
     bool        m_trace;
     std::string m_trace_file_name;
diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
new file mode 100644
index 000000000..bfade815c
--- /dev/null
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -0,0 +1,120 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    interpolant_cmds.cpp
+
+Abstract:
+    Commands for interpolation.
+
+Author:
+
+    Leonardo (leonardo) 2011-12-23
+
+Notes:
+
+--*/
+#include<sstream>
+#include"cmd_context.h"
+#include"cmd_util.h"
+#include"scoped_timer.h"
+#include"scoped_ctrl_c.h"
+#include"cancel_eh.h"
+#include"ast_pp.h"
+#include"ast_smt_pp.h"
+#include"ast_smt2_pp.h"
+#include"parametric_cmd.h"
+#include"mpq.h"
+#include"expr2var.h"
+#include"pp.h"
+#include"pp_params.hpp"
+#include"iz3interp.h"
+#include"iz3checker.h"
+
+static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, bool check) {
+
+  // get the proof, if there is one
+
+  if (!ctx.produce_interpolants())
+    throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
+  if (!ctx.has_manager() ||
+      ctx.cs_state() != cmd_context::css_unsat)
+    throw cmd_exception("proof is not available");
+  expr_ref pr(ctx.m());
+  pr = ctx.get_check_sat_result()->get_proof();
+  if (pr == 0)
+    throw cmd_exception("proof is not available");
+
+  // get the assertions
+
+  ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+  ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+  ptr_vector<ast> cnsts(end - it);
+  for (int i = 0; it != end; ++it, ++i)
+  cnsts[i] = *it;
+    
+  // compute an interpolant
+  
+  ptr_vector<ast> interps;
+ 
+  try {
+    iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
+  }
+  catch (iz3_bad_tree &) {
+    throw cmd_exception("interpolation pattern contains non-asserted formula");
+  }
+  catch (iz3_incompleteness &) {
+    throw cmd_exception("incompleteness in interpolator");
+  }
+
+  
+  // if we lived, print it out
+  for(unsigned i = 0; i < interps.size(); i++){
+    ctx.regular_stream()  << mk_pp(interps[i], ctx.m()) << std::endl;
+#if 0
+    ast_smt_pp pp(ctx.m());
+    pp.set_logic(ctx.get_logic().str().c_str());
+    pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
+    ctx.regular_stream() << std::endl;
+#endif
+  }
+
+  // verify, for the paranoid...
+  if(check || ctx.check_interpolants()){
+    std::ostringstream err;
+    ast_manager &_m = ctx.m();
+
+    // need a solver -- make one here FIXME is this right?
+    bool proofs_enabled, models_enabled, unsat_core_enabled;
+    params_ref p;
+    ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
+    scoped_ptr<solver> sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());
+
+    if(iz3check(_m,sp.get(),err,cnsts,t,interps))
+      ctx.regular_stream() << "correct\n";
+    else 
+      ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
+  }
+
+  for(unsigned i = 0; i < interps.size(); i++){
+    ctx.m().dec_ref(interps[i]);
+  }
+}
+
+static void get_interpolant(cmd_context & ctx, expr * t) {
+  get_interpolant_and_maybe_check(ctx,t,false);
+}
+
+static void get_and_check_interpolant(cmd_context & ctx, expr * t) {
+  get_interpolant_and_maybe_check(ctx,t,true);
+}
+
+UNARY_CMD(get_interpolant_cmd, "get-interpolant", "<fmla>", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
+
+// UNARY_CMD(get_and_check_interpolant_cmd, "get-and-check-interpolant", "<fmla>", "get and check interpolant for marked positions in fmla", CPK_EXPR, expr *, get_and_check_interpolant(ctx, arg););
+
+void install_interpolant_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(get_interpolant_cmd));
+    //    ctx.insert(alloc(get_and_check_interpolant_cmd));
+}
diff --git a/src/cmd_context/interpolant_cmds.h b/src/cmd_context/interpolant_cmds.h
new file mode 100644
index 000000000..d7ceb5dc2
--- /dev/null
+++ b/src/cmd_context/interpolant_cmds.h
@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    interpolant_cmds.h
+
+Abstract:
+    Commands for interpolation.
+
+Author:
+
+    Leonardo (leonardo) 2011-12-23
+
+Notes:
+
+--*/
+#ifndef _INTERPOLANT_CMDS_H_
+#define _INTERPOLANT_CMDS_H_
+
+class cmd_context;
+void install_interpolant_cmds(cmd_context & ctx);
+
+#endif
diff --git a/src/interp/foci2.h b/src/interp/foci2.h
new file mode 100755
index 000000000..261dd05dc
--- /dev/null
+++ b/src/interp/foci2.h
@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    foci2.h
+
+Abstract:
+
+   An interface class for foci2.   
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#ifndef FOCI2_H
+#define FOCI2_H
+
+#include <vector>
+#include <string>
+
+#ifdef WIN32
+#define FOCI2_EXPORT __declspec(dllexport)
+#else
+#define FOCI2_EXPORT __attribute__ ((visibility ("default")))
+#endif
+
+class foci2 {
+ public:
+  virtual ~foci2(){}
+
+  typedef int ast;
+  typedef int symb;
+
+  /** Built-in operators */
+  enum ops {
+    And = 0, Or, Not, Iff, Ite, Equal, Plus, Times, Floor, Leq, Div, Bool, Int, Array, Tsym, Fsym, Forall, Exists, Distinct, LastOp
+  };
+  
+  virtual symb mk_func(const std::string &s) = 0;
+  virtual symb mk_pred(const std::string &s) = 0;
+  virtual ast mk_op(ops op, const std::vector<ast> args) = 0;
+  virtual ast mk_op(ops op, ast) = 0;
+  virtual ast mk_op(ops op, ast, ast) = 0;
+  virtual ast mk_op(ops op, ast, ast, ast) = 0;
+  virtual ast mk_int(const std::string &) = 0;
+  virtual ast mk_rat(const std::string &) = 0;
+  virtual ast mk_true() = 0;
+  virtual ast mk_false() = 0;
+  virtual ast mk_app(symb,const std::vector<ast> args) = 0;
+  
+  virtual bool get_func(ast, symb &) = 0;
+  virtual bool get_pred(ast, symb &) = 0;
+  virtual bool get_op(ast, ops &) = 0;
+  virtual bool get_true(ast id) = 0;
+  virtual bool get_false(ast id) = 0;
+  virtual bool get_int(ast id, std::string &res) = 0;
+  virtual bool get_rat(ast id, std::string &res) = 0;
+  virtual const std::string &get_symb(symb) = 0;
+  
+  virtual int get_num_args(ast) = 0;
+  virtual ast get_arg(ast, int) = 0;
+  
+  virtual void show_ast(ast) = 0;
+  
+  virtual bool interpolate(const std::vector<ast> &frames, std::vector<ast> &itps, std::vector<int> parents) = 0;
+
+  FOCI2_EXPORT static foci2 *create(const std::string &);
+};
+
+#endif
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 51bf59798..e39dc9513 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -84,10 +84,9 @@ iz3base::range &iz3base::ast_scope(ast t){
 
 void iz3base::print(const std::string &filename){
   ast t = make(And,cnsts);
-  assert(0 && "not implemented");
-  // Z3_string smt = Z3_benchmark_to_smtlib_string(ctx,"iZ3","QFLIA","unsat","",0,0,t);  
-  // std::ofstream f(filename.c_str());
-  // f << smt;
+  std::ofstream f(filename.c_str());
+  print_sat_problem(f,t);
+  f.close();
 }
 
 
@@ -246,3 +245,76 @@ bool iz3base::is_sat(ast f){
 #endif
 }
 
+
+void iz3base::find_children(const hash_set<ast> &cnsts_set,
+			    const ast &tree,
+			    std::vector<ast> &cnsts,
+			    std::vector<int> &parents,
+			    std::vector<ast> &conjuncts,
+			    std::vector<int> &children,
+			    std::vector<int> &pos_map,
+			    bool merge
+			    ){
+  std::vector<int> my_children;
+  std::vector<ast> my_conjuncts;
+  if(op(tree) == Interp){ // if we've hit an interpolation position...
+    find_children(cnsts_set,arg(tree,0),cnsts,parents,my_conjuncts,my_children,pos_map,merge);
+    if(my_conjuncts.empty()) 
+      my_conjuncts.push_back(mk_true()); // need at least one conjunct
+    int root = cnsts.size() + my_conjuncts.size() - 1;
+    for(unsigned i = 0; i < my_conjuncts.size(); i++){
+      parents.push_back(root);
+      cnsts.push_back(my_conjuncts[i]);
+    }
+    for(unsigned i = 0; i < my_children.size(); i++)
+      parents[my_children[i]] = root;
+    children.push_back(root);
+    pos_map.push_back(root);
+  }
+  else {
+    if(op(tree) == And){
+      int nargs = num_args(tree);
+      for(int i = 0; i < nargs; i++)
+	find_children(cnsts_set,arg(tree,i),cnsts,parents,my_conjuncts,my_children,pos_map,merge);
+    }
+    if(cnsts_set.find(tree) != cnsts_set.end()){
+      if(merge && !my_conjuncts.empty())
+	my_conjuncts.back() = mk_and(my_conjuncts.back(),tree);
+      else
+	my_conjuncts.push_back(tree);
+    }
+    for(unsigned i = 0; i < my_children.size(); i++)
+      children.push_back(my_children[i]);
+    for(unsigned i = 0; i < my_conjuncts.size(); i++)
+      conjuncts.push_back(my_conjuncts[i]);
+  }
+}
+    
+void iz3base::to_parents_vec_representation(const std::vector<ast> &_cnsts,
+					    const ast &tree,
+					    std::vector<ast> &cnsts,
+					    std::vector<int> &parents,
+					    std::vector<ast> &theory,
+					    std::vector<int> &pos_map,
+					    bool merge
+					    ){
+  std::vector<int> my_children;
+  std::vector<ast> my_conjuncts;
+  hash_set<ast> cnsts_set;
+  for(unsigned i = 0; i < _cnsts.size(); i++)
+    cnsts_set.insert(_cnsts[i]);
+  ast _tree = (op(tree) != Interp) ? make(Interp,tree) : tree;
+  find_children(cnsts_set,_tree,cnsts,parents,my_conjuncts,my_children,pos_map,merge);
+  if(op(tree) != Interp) pos_map.pop_back();
+  parents[parents.size()-1] = SHRT_MAX;
+    
+  // rest of the constraints are the background theory
+    
+  hash_set<ast> used_set;
+  for(unsigned i = 0; i < cnsts.size(); i++)
+    used_set.insert(cnsts[i]);
+  for(unsigned i = 0; i < _cnsts.size(); i++)
+    if(used_set.find(_cnsts[i]) == used_set.end())
+      theory.push_back(_cnsts[i]);
+}
+
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index b379be30c..da0a3ce4a 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -65,7 +65,7 @@ class iz3base : public iz3mgr, public scopes {
     weak = false;
   }
 
- iz3base(const iz3mgr& other,
+  iz3base(const iz3mgr& other,
 	 const std::vector<ast> &_cnsts,
 	 const std::vector<int> &_parents,
 	 const std::vector<ast> &_theory)
@@ -74,6 +74,11 @@ class iz3base : public iz3mgr, public scopes {
     weak = false;
   }
 
+  iz3base(const iz3mgr& other)
+   : iz3mgr(other), scopes()  {
+    weak = false;
+  }
+
   /* Set our options */
   void set_option(const std::string &name, const std::string &value){
     if(name == "weak" && value == "1") weak = true;
@@ -102,6 +107,19 @@ class iz3base : public iz3mgr, public scopes {
     return make(And,cs);
   }
   
+  void to_parents_vec_representation(const std::vector<ast> &_cnsts,
+				     const ast &tree,
+				     std::vector<ast> &cnsts,
+				     std::vector<int> &parents,
+				     std::vector<ast> &theory,
+				     std::vector<int> &pos_map,
+				     bool merge = false
+				   );
+
+ protected:
+  std::vector<ast> cnsts;
+  std::vector<ast> theory;
+
  private:
 
   struct ranges {
@@ -120,8 +138,6 @@ class iz3base : public iz3mgr, public scopes {
 
   void initialize(const std::vector<ast> &_parts, const std::vector<int> &_parents, const std::vector<ast> &_theory);
 
-  std::vector<ast> cnsts;
-  std::vector<ast> theory;
 
   bool is_literal(ast n);
   void gather_conjuncts_rec(ast n, std::vector<ast> &conjuncts, stl_ext::hash_set<ast> &memo);
@@ -129,7 +145,15 @@ class iz3base : public iz3mgr, public scopes {
   ast simplify_and(std::vector<ast> &conjuncts);
   ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth);
   ast simplify_with_lit(ast n, ast lit);  
-
+  void find_children(const stl_ext::hash_set<ast> &cnsts_set,
+		     const ast &tree,
+		     std::vector<ast> &cnsts,
+		     std::vector<int> &parents,
+		     std::vector<ast> &conjuncts,
+		     std::vector<int> &children,
+		     std::vector<int> &pos_map,
+		     bool merge
+		     );
   bool weak;
 
 };
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
new file mode 100755
index 000000000..b30e52d38
--- /dev/null
+++ b/src/interp/iz3checker.cpp
@@ -0,0 +1,192 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+   iz3checker.cpp
+
+Abstract:
+
+   check correctness of interpolant
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#include "iz3base.h"
+#include "iz3checker.h"
+
+#include <algorithm>
+#include <stdio.h>
+#include <fstream>
+#include <sstream>
+#include <iostream>
+#include <set>
+#include <iterator>
+
+
+#ifndef WIN32
+using namespace stl_ext;
+#endif
+
+struct iz3checker : iz3base {
+  
+  /* HACK: for tree interpolants, we assume that uninterpreted functions
+     are global. This is because in the current state of the tree interpolation
+     code, symbols that appear in sibling sub-trees have to be global, and
+     we have no way to eliminate such function symbols. When tree interpoaltion is
+     fixed, we can tree function symbols the same as constant symbols. */
+
+  bool is_tree;
+
+  void support(const ast &t, std::set<std::string> &res, hash_set<ast> &memo){
+    if(memo.find(t) != memo.end()) return;
+    memo.insert(t);
+    
+    int nargs = num_args(t);
+    for(int i = 0; i < nargs; i++)
+      support(arg(t,i),res,memo);
+    
+    switch(op(t)){
+    case Uninterpreted:
+      if(nargs == 0 || !is_tree) {
+	std::string name = string_of_symbol(sym(t));
+	res.insert(name);
+      }
+      break;
+    case Forall:
+    case Exists:
+      support(get_quantifier_body(t),res,memo);
+      break;
+    default:;
+    }
+  }
+
+  bool check(solver *s, std::ostream &err,
+	     const std::vector<ast> &cnsts,
+	     const std::vector<int> &parents,
+	     const std::vector<ast> &itp,
+	     const std::vector<ast> &theory){
+
+    is_tree = !parents.empty();
+    int num = cnsts.size();
+    std::vector<std::vector<int> > children(num);
+  
+    for(int i = 0; i < num-1; i++){
+      if(parents.size())
+	children[parents[i]].push_back(i);
+      else 
+	children[i+1].push_back(i);
+    }
+
+    for(int i = 0; i < num; i++){
+      s->push();
+      for(unsigned j = 0; j < theory.size(); j++)
+	s->assert_expr(to_expr(theory[j].raw()));
+      s->assert_expr(to_expr(cnsts[i].raw()));
+      std::vector<int> &cs = children[i];
+      for(unsigned j = 0; j < cs.size(); j++)
+	s->assert_expr(to_expr(itp[cs[j]].raw()));
+      if(i != num-1)
+	s->assert_expr(to_expr(mk_not(itp[i]).raw()));
+      lbool result = s->check_sat(0,0);
+      if(result != l_false){
+	err << "interpolant " << i << " is incorrect";
+	return false;
+      }
+      s->pop(1);
+    }
+
+    std::vector<std::set<std::string> > supports(num);
+    for(int i = 0; i < num; i++){
+      hash_set<ast> memo;
+      support(cnsts[i],supports[i],memo);
+    }
+    for(int i = 0; i < num-1; i++){
+      std::vector<bool> Bside(num);
+      for(int j = num-1; j >= 0; j--)
+	Bside[j] = j != i;
+      for(int j = num-1; j >= 0; j--)
+	if(!Bside[j]){
+	  std::vector<int> &cs = children[i];
+	  for(unsigned k = 0; k < cs.size(); k++)
+	    Bside[cs[k]] = false;
+	}
+      std::set<std::string> Asup, Bsup,common,Isup,bad;
+      for(int j = num-1; j >= 0; j--){
+	std::set<std::string> &side = Bside[j] ? Bsup : Asup;
+	side.insert(supports[j].begin(),supports[j].end());
+      }
+      std::set_intersection(Asup.begin(),Asup.end(),Bsup.begin(),Bsup.end(),std::inserter(common,common.begin()));
+      {
+	hash_set<ast> tmemo;
+	for(unsigned j = 0; j < theory.size(); j++)
+	  support(theory[j],common,tmemo);                // all theory symbols allowed in interps
+      }	
+      hash_set<ast> memo;
+      support(itp[i],Isup,memo);
+      std::set_difference(Isup.begin(),Isup.end(),common.begin(),common.end(),std::inserter(bad,bad.begin()));
+      if(!bad.empty()){
+	err << "bad symbols in interpolant " << i << ":";
+	std::copy(bad.begin(),bad.end(),std::ostream_iterator<std::string>(err,","));
+	return false;
+      }
+    }
+    return true;
+  }
+  
+  bool check(solver *s, std::ostream &err,
+	     const std::vector<ast> &_cnsts,
+	     const ast &tree,
+	     const std::vector<ast> &itp){
+
+    std::vector<int> pos_map;
+    
+    // convert to the parents vector representation
+    
+    to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
+    
+    //use the parents vector representation to compute interpolant
+    return check(s,err,cnsts,parents,itp,theory);
+  }
+
+  iz3checker(ast_manager &_m)
+    : iz3base(_m) {
+  }
+};  
+
+template <class T>
+std::vector<T> to_std_vector(const ::vector<T> &v){
+  std::vector<T> _v(v.size());
+  for(unsigned i = 0; i < v.size(); i++)
+    _v[i] = v[i];
+  return _v;
+}
+
+
+bool iz3check(ast_manager &_m_manager,
+	      solver *s,
+	      std::ostream &err,
+	      const ptr_vector<ast> &cnsts,
+	      const ::vector<int> &parents,
+	      const ptr_vector<ast> &interps,
+	      const ptr_vector<ast> &theory)
+{
+  iz3checker chk(_m_manager);
+  return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory));
+}
+
+bool iz3check(ast_manager &_m_manager,
+	      solver *s,
+	      std::ostream &err,
+	      const ptr_vector<ast> &_cnsts,
+	      ast *tree,
+	      const ptr_vector<ast> &interps)
+{
+  iz3checker chk(_m_manager);
+  return chk.check(s,err,chk.cook(_cnsts),chk.cook(tree),chk.cook(interps));
+}
diff --git a/src/interp/iz3checker.h b/src/interp/iz3checker.h
new file mode 100644
index 000000000..5402e4d68
--- /dev/null
+++ b/src/interp/iz3checker.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+   iz3checker.h
+
+Abstract:
+
+   check correctness of an interpolant
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#ifndef IZ3_CHECKER_H
+#define IZ3_CHECKER_H
+
+#include "iz3mgr.h"
+#include "solver.h"
+
+bool iz3check(ast_manager &_m_manager,
+	      solver *s,
+	      std::ostream &err,
+	      const ptr_vector<ast> &cnsts,
+	      const ::vector<int> &parents,
+	      const ptr_vector<ast> &interps,
+	      const ptr_vector<ast> &theory);
+
+bool iz3check(ast_manager &_m_manager,
+	      solver *s,
+	      std::ostream &err,
+	      const ptr_vector<ast> &cnsts,
+	      ast *tree,
+	      const ptr_vector<ast> &interps);
+
+#endif
diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index 53e4ec84b..38f588ce3 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -158,6 +158,7 @@ public:
       case Numeral: {
 	std::string s = string_of_numeral(t);
 	res = foci->mk_int(s);
+	break;
       }
       case Forall: 
       case Exists: {
@@ -177,12 +178,14 @@ public:
 	foci_bvs.push_back(body);
 	res = foci->mk_op(qop,foci_bvs);
 	node_to_ast[res] = t; // desperate
+	break;
       }
       case Variable: {  // a deBruijn index
         int index = get_variable_index_value(t);
 	type ty = get_type(t);
         foci2::symb symbol = make_deBruijn_symbol(index,ty);
         res = foci->mk_app(symbol,std::vector<foci2::ast>());
+	break;
       }
       default:
 	{
@@ -240,7 +243,7 @@ public:
       case foci2::Times:
 	res = make(Times,args); break; 
       case foci2::Div:
-	res = make(Div,args[0],args[1]); break;
+	res = make(Idiv,args[0],args[1]); break;
       case foci2::Leq:
 	res = make(Leq,args[0],args[1]); break; 
       case foci2::Distinct:
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 6da83004d..f3bde143d 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -34,6 +34,7 @@ Revision History:
 #include "iz3interp.h"
 
 
+
 #ifndef WIN32
 using namespace stl_ext;
 #endif
@@ -164,9 +165,32 @@ static lbool test_secondary(context ctx,
 }                         
 #endif
     
+template<class T>
+struct killme {
+  T *p;
+  killme(){p = 0;}
+  void set(T *_p) {p = _p;} 
+  ~killme(){
+    if(p)
+      delete p;
+  }
+};
 
-class iz3interp : public iz3mgr {
+
+class iz3interp : public iz3base {
 public:
+
+  killme<iz3secondary> sp_killer;
+  killme<iz3translation> tr_killer;
+
+  bool is_linear(std::vector<int> &parents){
+    for(int i = 0; i < ((int)parents.size())-1; i++)
+      if(parents[i] != i+1)
+	return false;
+    return true;
+  }
+
+
   void proof_to_interpolant(z3pf proof,
 			    const std::vector<ast> &cnsts,
 			    const std::vector<int> &parents,
@@ -187,11 +211,17 @@ public:
     int num = cnsts_vec.size();
     std::vector<ast> interps_vec(num-1);
     
+    // if this is really a sequence problem, we can make it easier
+    if(is_linear(parents_vec))
+      parents_vec.clear();
+
     // create a secondary prover
     iz3secondary *sp = iz3foci::create(this,num,parents_vec.empty()?0:&parents_vec[0]);
+    sp_killer.set(sp); // kill this on exit
 	  
     // create a translator
     iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory);
+    tr_killer.set(tr);
     
     // set the translation options, if needed
     if(options)
@@ -220,12 +250,37 @@ public:
     fr.fix_interpolants(interps_vec);
 
     interps = interps_vec;
-    delete tr;
-    delete sp;
   }
 
+
+  // same as above, but represents the tree using an ast
+
+  void proof_to_interpolant(const z3pf &proof,
+			    const std::vector<ast> &_cnsts,
+			    const ast &tree,
+			    std::vector<ast> &interps,
+			    interpolation_options_struct *options = 0
+			    ){
+    std::vector<int> pos_map;
+    
+    // convert to the parents vector representation
+    
+    to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
+
+    
+    //use the parents vector representation to compute interpolant
+    proof_to_interpolant(proof,cnsts,parents,interps,theory,options);
+    
+    // get the interps for the tree positions
+    std::vector<ast> _interps = interps;
+    interps.resize(pos_map.size());
+    for(unsigned i = 0; i < pos_map.size(); i++)
+      interps[i] = i < _interps.size() ? _interps[i] : mk_false();
+  }
+
+
   iz3interp(ast_manager &_m_manager)
-    : iz3mgr(_m_manager) {}
+    : iz3base(_m_manager) {}
 };
 
 void iz3interpolate(ast_manager &_m_manager,
@@ -254,3 +309,26 @@ void iz3interpolate(ast_manager &_m_manager,
     interps[i] = itp.uncook(_interps[i]);
 }
 
+void iz3interpolate(ast_manager &_m_manager,
+		    ast *proof,
+		    const ptr_vector<ast> &cnsts,
+		    ast *tree,
+		    ptr_vector<ast> &interps,
+		    interpolation_options_struct * options)
+{
+  iz3interp itp(_m_manager);
+  std::vector<iz3mgr::ast> _cnsts(cnsts.size());
+  std::vector<iz3mgr::ast> _interps;
+  for(unsigned i = 0; i < cnsts.size(); i++)
+    _cnsts[i] = itp.cook(cnsts[i]);
+  iz3mgr::ast _proof = itp.cook(proof);
+  iz3mgr::ast _tree = itp.cook(tree);
+  itp.proof_to_interpolant(_proof,_cnsts,_tree,_interps,options);
+  interps.resize(_interps.size());
+  for(unsigned i = 0; i < interps.size(); i++)
+    interps[i] = itp.uncook(_interps[i]);
+}
+
+
+
+
diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h
index d87aefba8..017791186 100644
--- a/src/interp/iz3interp.h
+++ b/src/interp/iz3interp.h
@@ -26,6 +26,14 @@ struct interpolation_options_struct {
   stl_ext::hash_map<std::string,std::string> map;
 };
 
+/** This object is thrown if a tree interpolation problem is mal-formed */
+struct iz3_bad_tree {
+};
+
+/** This object is thrown when iz3 fails due to an incompleteness in
+    the secondary solver. */
+struct iz3_incompleteness {
+};
 
 typedef interpolation_options_struct *interpolation_options;
 
@@ -37,4 +45,11 @@ void iz3interpolate(ast_manager &_m_manager,
 		    const ptr_vector<ast> &theory,
 		    interpolation_options_struct * options = 0);
 
+void iz3interpolate(ast_manager &_m_manager,
+		    ast *proof,
+		    const ptr_vector<ast> &cnsts,
+		    ast *tree,
+		    ptr_vector<ast> &interps,
+		    interpolation_options_struct * options);
+
 #endif
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index fd9b17edc..807c38227 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -57,6 +57,7 @@ iz3mgr::ast iz3mgr::make(opr op, int n, raw_ast **args){
   case Not:      return mki(m_basic_fid,OP_NOT,n,args);
   case Implies:  return mki(m_basic_fid,OP_IMPLIES,n,args);
   case Oeq:      return mki(m_basic_fid,OP_OEQ,n,args);
+  case Interp:   return mki(m_basic_fid,OP_INTERP,n,args);
   case Leq:      return mki(m_arith_fid,OP_LE,n,args);
   case Geq:      return mki(m_arith_fid,OP_GE,n,args);
   case Lt:       return mki(m_arith_fid,OP_LT,n,args);
@@ -107,7 +108,7 @@ iz3mgr::ast iz3mgr::make(opr op){
   return make(op,0,0);
 }
 
-iz3mgr::ast iz3mgr::make(opr op, ast &arg0){
+iz3mgr::ast iz3mgr::make(opr op, const ast &arg0){
   raw_ast *a = arg0.raw();
   return make(op,1,&a);
 }
@@ -119,7 +120,7 @@ iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1){
   return make(op,2,args);
 }
 
-iz3mgr::ast iz3mgr::make(opr op, ast &arg0, ast &arg1, ast &arg2){
+iz3mgr::ast iz3mgr::make(opr op, const ast &arg0, const ast &arg1, const ast &arg2){
   raw_ast *args[3];
   args[0] = arg0.raw();
   args[1] = arg1.raw();
@@ -335,13 +336,11 @@ void iz3mgr::pretty_print(std::ostream &f, const std::string &s){
 }
 
 
-iz3mgr::opr iz3mgr::op(ast &t){
+iz3mgr::opr iz3mgr::op(const ast &t){
     ast_kind dk = t.raw()->get_kind();
     switch(dk){
     case AST_APP: {
       expr * e = to_expr(t.raw());
-      if (m().is_unique_value(e)) 
-	return Numeral;
       func_decl *d = to_app(t.raw())->get_decl();
       if (null_family_id == d->get_family_id())
 	return Uninterpreted;
@@ -360,6 +359,7 @@ iz3mgr::opr iz3mgr::op(ast &t){
 	case OP_NOT:      return Not;
 	case OP_IMPLIES:  return Implies;
 	case OP_OEQ:      return Oeq;
+	case OP_INTERP:   return Interp;
 	default:
 	  return Other;
         }
@@ -383,6 +383,8 @@ iz3mgr::opr iz3mgr::op(ast &t){
 	case OP_TO_INT: return ToInt;
 	case OP_IS_INT: return IsInt;
 	default:
+	  if (m().is_unique_value(e)) 
+	    return Numeral;
 	  return Other;
 	  }
       }
@@ -423,3 +425,9 @@ iz3mgr::pfrule iz3mgr::pr(const ast &t){
   assert(m_basic_fid == d->get_family_id());
   return d->get_decl_kind();
 }
+
+void iz3mgr::print_sat_problem(std::ostream &out, const ast &t){
+  ast_smt_pp pp(m());
+  pp.set_simplify_implies(false);
+  pp.display_smt2(out, to_expr(t.raw()));
+}
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 4f247bb81..3317b9d7d 100644
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -130,7 +130,7 @@ namespace std {
     class less<ast_r> {
   public:
     size_t operator()(const ast_r &s, const ast_r &t) const {
-      return s.raw()->get_id() < t.raw()->get_id();
+      return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
     }
   };
 }
@@ -161,6 +161,7 @@ class iz3mgr  {
     Distinct,
     Xor,
     Oeq,
+    Interp,
     Leq,
     Geq,
     Lt,
@@ -196,7 +197,7 @@ class iz3mgr  {
     Other
   };
 
-  opr op(ast &t);
+  opr op(const ast &t);
 
   unsigned ast_id(const ast &x)
   {
@@ -208,9 +209,9 @@ class iz3mgr  {
   ast make_var(const std::string &name, type ty);
   ast make(opr op, const std::vector<ast> &args);
   ast make(opr op);
-  ast make(opr op, ast &arg0);
+  ast make(opr op, const ast &arg0);
   ast make(opr op, const ast &arg0, const ast &arg1);
-  ast make(opr op, ast &arg0, ast &arg1, ast &arg2);
+  ast make(opr op, const ast &arg0, const ast &arg1, const ast &arg2);
   ast make(symb sym, const std::vector<ast> &args);
   ast make(symb sym);
   ast make(symb sym, ast &arg0);
@@ -223,6 +224,13 @@ class iz3mgr  {
 
   ast cook(raw_ast *a) {return ast(&m_manager,a);}
 
+  std::vector<ast> cook(ptr_vector<raw_ast> v) {
+    std::vector<ast> _v(v.size());
+    for(unsigned i = 0; i < v.size(); i++)
+      _v[i] = cook(v[i]);
+    return _v;
+  }
+
   raw_ast *uncook(const ast &a) {
     m_manager.inc_ref(a.raw());
     return a.raw();
@@ -245,7 +253,7 @@ class iz3mgr  {
     assert(0);
   }
 
-  ast arg(ast t, int i){
+  ast arg(const ast &t, int i){
     ast_kind dk = t.raw()->get_kind();
     switch(dk){
     case AST_APP:
@@ -427,6 +435,8 @@ class iz3mgr  {
 
   void print_clause(std::ostream &s, std::vector<ast> &cls);
 
+  void print_sat_problem(std::ostream &out, const ast &t);
+
   void show_clause(std::vector<ast> &cls);
 
   static void pretty_print(std::ostream &f, const std::string &s);
diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp
new file mode 100644
index 000000000..1f9351453
--- /dev/null
+++ b/src/interp/iz3pp.cpp
@@ -0,0 +1,175 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+   iz3pp.cpp
+
+Abstract:
+
+   Pretty-print interpolation problems
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+/* Copyright 2011 Microsoft Research. */
+#include <assert.h>
+#include <algorithm>
+#include <stdio.h>
+#include <fstream>
+#include <sstream>
+#include <set>
+#include <iostream>
+
+#include "iz3mgr.h"
+#include "iz3pp.h"
+#include "func_decl_dependencies.h"
+#include"for_each_expr.h"
+#include"ast_smt_pp.h"
+#include"ast_smt2_pp.h"
+#include"expr_functors.h"
+#include"expr_abstract.h"
+
+
+#ifndef WIN32
+using namespace stl_ext;
+#endif
+
+// TBD: algebraic data-types declarations will not be printed.
+class free_func_visitor {
+  ast_manager& m;
+  func_decl_set m_funcs;
+  obj_hashtable<sort> m_sorts;
+public:        
+  free_func_visitor(ast_manager& m): m(m) {}
+  void operator()(var * n)        { }
+  void operator()(app * n)        { 
+    m_funcs.insert(n->get_decl()); 
+    sort* s = m.get_sort(n);
+    if (s->get_family_id() == null_family_id) {
+      m_sorts.insert(s);
+    }
+  }
+  void operator()(quantifier * n) { }
+  func_decl_set& funcs() { return m_funcs; }
+  obj_hashtable<sort>& sorts() { return m_sorts; }
+};
+
+class iz3pp_helper : public iz3mgr {
+public:
+  
+  void print_tree(const ast &tree, hash_map<expr*,symbol> &cnames, std::ostream &out){
+    hash_map<expr*,symbol>::iterator foo = cnames.find(to_expr(tree.raw()));
+    if(foo != cnames.end()){
+      symbol nm = foo->second;
+      if (is_smt2_quoted_symbol(nm)) {
+	out << mk_smt2_quoted_symbol(nm);
+      }
+      else {
+	out << nm;
+      }
+    }
+    else if(op(tree) == And){
+      out << "(and";
+      int nargs = num_args(tree);
+      for(int i = 0; i < nargs; i++){
+	out << " ";
+	print_tree(arg(tree,i), cnames, out);
+      }
+      out << ")";
+    }
+    else if(op(tree) == Interp){
+      out << "(interp ";
+      print_tree(arg(tree,0), cnames, out);
+      out << ")";
+    }
+    else throw iz3pp_bad_tree();
+  }
+
+
+  iz3pp_helper(ast_manager &_m_manager)
+    : iz3mgr(_m_manager) {}
+};
+
+void iz3pp(ast_manager &m,
+	   const ptr_vector<expr> &cnsts_vec,
+	   expr *tree,
+	   std::ostream& out) {
+
+  unsigned sz = cnsts_vec.size();
+  expr* const* cnsts = &cnsts_vec[0];
+
+  out << "(set-option :produce-interpolants true)\n";
+
+  free_func_visitor visitor(m);
+  expr_mark visited;
+  bool print_low_level = true; // m_params.print_low_level_smt2();
+  
+#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
+  
+  smt2_pp_environment_dbg env(m);
+
+  for (unsigned i = 0; i < sz; ++i) {
+    expr* e = cnsts[i];
+    for_each_expr(visitor, visited, e);
+  }
+  
+  // name all the constraints
+  hash_map<expr *, symbol> cnames;
+  int ctr = 1;
+  for(unsigned i = 0; i < sz; i++){
+    symbol nm;
+    std::ostringstream s;
+    s << "f!" << (ctr++);
+    cnames[cnsts[i]] = symbol(s.str().c_str());
+  }
+  
+  func_decl_set &funcs = visitor.funcs();
+  func_decl_set::iterator it  = funcs.begin(), end = funcs.end();
+  
+  obj_hashtable<sort>& sorts = visitor.sorts();
+  obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
+  
+
+  
+  for (; sit != send; ++sit) {
+    PP(*sit);
+  }
+  
+  for (; it != end; ++it) {
+    func_decl* f = *it;
+    if(f->get_family_id() == null_family_id){
+      PP(f);
+      out << "\n";
+    }
+  }
+  
+  for (unsigned i = 0; i < sz; ++i) {            
+    out << "(assert ";
+    expr* r = cnsts[i];
+    symbol nm = cnames[r];
+    out << "(! ";
+    PP(r);
+    out << " :named ";
+    if (is_smt2_quoted_symbol(nm)) {
+      out << mk_smt2_quoted_symbol(nm);
+    }
+    else {
+      out << nm;
+    }
+    out << ")";
+    out << ")\n";
+  }
+  out << "(check-sat)\n";
+  out << "(get-interpolant ";
+  iz3pp_helper pp(m);
+  pp.print_tree(pp.cook(tree),cnames,out);
+  out << ")\n";
+}
+
+
diff --git a/src/interp/iz3pp.h b/src/interp/iz3pp.h
new file mode 100644
index 000000000..3ea5925e8
--- /dev/null
+++ b/src/interp/iz3pp.h
@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+   iz3pp.cpp
+
+Abstract:
+
+   Pretty-print interpolation problems
+
+Author:
+
+    Ken McMillan (kenmcmil)
+
+Revision History:
+
+--*/
+
+#ifndef IZ3_PP_H
+#define IZ3_PP_H
+
+#include "iz3mgr.h"
+
+/** Exception thrown in case of mal-formed tree interpoloation
+    specification */
+
+struct iz3pp_bad_tree {
+};
+
+void iz3pp(ast_manager &m,
+	   const ptr_vector<expr> &cnsts_vec,
+	   expr *tree,
+	   std::ostream& out);
+#endif
diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h
index 2ba3a999f..6e2261d0c 100755
--- a/src/interp/iz3scopes.h
+++ b/src/interp/iz3scopes.h
@@ -32,6 +32,13 @@ class scopes {
     parents = _parents;
   }
 
+  scopes(){
+  }
+  
+  void initialize(const std::vector<int> &_parents){
+    parents = _parents;
+  }
+
   /** The parents vector defining the tree structure */
   std::vector<int> parents;
 
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index a16d079c8..d4656d3a8 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include "iz3translate.h"
 #include "iz3proof.h"
 #include "iz3profiling.h"
+#include "iz3interp.h"
 
 #include <assert.h>
 #include <algorithm>
@@ -336,6 +337,16 @@ public:
 	}	    
       }
     }
+#if 0
+    AstSet::iterator it = res.begin(), en = res.end();
+    if(it != en){
+      AstSet::iterator old = it;
+      ++it;
+      for(; it != en; ++it, ++old)
+	if(!(*old < *it))
+	  std::cout << "foo!";
+    }
+#endif
     return res;
   }
 
@@ -439,25 +450,28 @@ public:
     if(it != localization_map.end())
       return it->second;
 
-    // if is is non-local, we must first localise the arguments to
+    // if is is non-local, we must first localize the arguments to
     // the range of its function symbol
-    if(op(e) == Uninterpreted){
-      symb f = sym(e);
-      range frng = sym_range(f);
-      int nargs = num_args(e);
-      if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
-	if(ranges_intersect(frng,rng)) // localize to desired range if possible
-	  {frng = range_glb(frng,rng);}
-	std::vector<ast> largs(nargs);
-	for(int i = 0; i < nargs; i++){
-	  largs[i] = localize_term(arg(e,i),frng);
-	  frng = range_glb(frng,ast_scope(largs[i]));
-	}
-	e = make(f,largs);
-	assert(is_local(e));
+    
+    int nargs = num_args(e);
+    if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
+      range frng = rng;
+      if(op(e) == Uninterpreted){
+	symb f = sym(e);
+	range srng = sym_range(f);
+	if(ranges_intersect(srng,rng)) // localize to desired range if possible
+	  frng = range_glb(srng,rng);
       }
+      std::vector<ast> largs(nargs);
+      for(int i = 0; i < nargs; i++){
+	largs[i] = localize_term(arg(e,i),frng);
+	frng = range_glb(frng,ast_scope(largs[i]));
+      }
+      e = clone(e,largs);
+      assert(is_local(e));
     }
 
+
     if(ranges_intersect(ast_scope(e),rng))
       return e; // this term occurs in range, so it's O.K.
 
@@ -774,10 +788,12 @@ public:
 
     // if sat, lemma isn't valid, something is wrong
     if(sat){
+#if 1
       std::cerr << "invalid lemma written to file invalid_lemma.smt:\n";
       iz3base foo(*this,preds,std::vector<int>(),std::vector<ast>());
       foo.print("invalid_lemma.smt");
-      throw invalid_lemma();
+#endif
+      throw iz3_incompleteness();
     }
     assert(sat == 0); // if sat, lemma doesn't hold!
 
@@ -961,12 +977,14 @@ public:
 	AstSet &this_hyps = get_hyps(proof);
 	if(std::includes(hyps.begin(),hyps.end(),this_hyps.begin(),this_hyps.end())){
 	  // if(hyps.find(con) == hyps.end())
+#if 0
           if(/* lemma_count == SHOW_LEMMA_COUNT - 1 && */ !is_literal_or_lit_iff(conc(proof))){
              std::cout << "\nnon-lit local ante\n";
              show_step(proof);
              show(conc(proof));
              throw non_lit_local_ante();
           }
+#endif
           local_antes.push_back(proof);
 	  return true;
 	}
@@ -1019,7 +1037,7 @@ public:
   std::vector<ast> lit_trace;
   hash_set<ast> marked_proofs;
 
-  bool proof_has_lit(ast proof, ast lit){
+  bool proof_has_lit(const ast &proof, const ast &lit){
     AstSet &hyps = get_hyps(proof);
     if(hyps.find(mk_not(lit)) != hyps.end())
       return true;
@@ -1033,7 +1051,7 @@ public:
   }
 
 
-  void trace_lit_rec(ast lit, ast proof, AstHashSet &memo){
+  void trace_lit_rec(const ast &lit, const ast &proof, AstHashSet &memo){
     if(memo.find(proof) == memo.end()){
       memo.insert(proof);
       AstSet &hyps = get_hyps(proof);
@@ -1064,7 +1082,7 @@ public:
   
   ast traced_lit;
 
-  int trace_lit(ast lit, ast proof){
+  int trace_lit(const ast &lit, const ast &proof){
     marked_proofs.clear();
     lit_trace.clear();
     traced_lit = lit;
@@ -1073,7 +1091,7 @@ public:
     return lit_trace.size();
   }
 
-  bool is_literal_or_lit_iff(ast lit){
+  bool is_literal_or_lit_iff(const ast &lit){
     if(my_is_literal(lit)) return true;
     if(op(lit) == Iff){
       return my_is_literal(arg(lit,0)) && my_is_literal(arg(lit,1));
@@ -1081,13 +1099,13 @@ public:
     return false;
   }
 
-  bool my_is_literal(ast lit){
+  bool my_is_literal(const ast &lit){
     ast abslit = is_not(lit) ? arg(lit,0) : lit;
     int f = op(abslit);
     return !(f == And || f == Or || f == Iff);
   }
 
-  void print_lit(ast lit){
+  void print_lit(const ast &lit){
     ast abslit = is_not(lit) ? arg(lit,0) : lit;
     if(!is_literal_or_lit_iff(lit)){
       if(is_not(lit)) std::cout << "~";
@@ -1099,22 +1117,22 @@ public:
       print_expr(std::cout,lit);
   }
 
-  void show_lit(ast lit){
+  void show_lit(const ast &lit){
     print_lit(lit);
     std::cout << "\n";
   }
 
-  void print_z3_lit(ast a){
+  void print_z3_lit(const ast &a){
     print_lit(from_ast(a));
   }
 
-  void show_z3_lit(ast a){
+  void show_z3_lit(const ast &a){
     print_z3_lit(a);
     std::cout << "\n";
   }
 
   
-  void show_con(ast proof, bool brief){
+  void show_con(const ast &proof, bool brief){
     if(!traced_lit.null() && proof_has_lit(proof,traced_lit))
       std::cout << "(*) ";
     ast con = conc(proof);
@@ -1138,7 +1156,7 @@ public:
     std::cout << "\n";
   }
 
-  void show_step( ast proof){
+  void show_step(const  ast &proof){
     std::cout << "\n";
     unsigned nprems = num_prems(proof);
     for(unsigned i = 0; i < nprems; i++){
@@ -1151,7 +1169,7 @@ public:
     show_con(proof,false);
   }
 
-  void show_marked( ast proof){
+  void show_marked( const ast &proof){
     std::cout << "\n";
     unsigned nprems = num_prems(proof);
     for(unsigned i = 0; i < nprems; i++){
@@ -1166,7 +1184,7 @@ public:
   std::vector<ast> pfhist;
   int pfhist_pos;
   
-  void pfgoto(ast proof){
+  void pfgoto(const ast &proof){
     if(pfhist.size() == 0)
       pfhist_pos = 0;
     else pfhist_pos++;
@@ -1245,7 +1263,7 @@ public:
     return res;
   }
 
-  Iproof::node extract_simple_proof(ast proof, hash_set<ast> &leaves){
+  Iproof::node extract_simple_proof(const ast &proof, hash_set<ast> &leaves){
     if(leaves.find(proof) != leaves.end())
       return iproof->make_hypothesis(conc(proof));
     ast con = from_ast(conc(proof));
@@ -1271,7 +1289,7 @@ public:
     return 0;
   }
 
-  int extract_th_lemma_simple(ast proof, std::vector<ast> &lits){
+  int extract_th_lemma_simple(const ast &proof, std::vector<ast> &lits){
     std::vector<ast> la = local_antes;
     local_antes.clear();  // clear antecedents for next lemma
     antes_added.clear();
@@ -1321,7 +1339,7 @@ public:
 
 // #define NEW_EXTRACT_TH_LEMMA
 
-  void get_local_hyps(ast proof, std::set<ast> &res){
+  void get_local_hyps(const ast &proof, std::set<ast> &res){
     std::set<ast> hyps = get_hyps(proof);
     for(std::set<ast>::iterator it = hyps.begin(), en = hyps.end(); it != en; ++it){
       ast hyp = *it;
@@ -1376,6 +1394,7 @@ public:
     try {
       res = extract_th_lemma_common(lits,nll,lemma_nll);
     }
+#if 0
     catch (const invalid_lemma &) {
       std::cout << "\n\nlemma: " << my_count;
       std::cout << "\n\nproof node: \n";
@@ -1397,6 +1416,7 @@ public:
         show_lit(lits[i]);
       throw invalid_lemma();
     }
+#endif
     
     return res;
 #else
@@ -1648,7 +1668,7 @@ public:
       if(!(res = extract_th_lemma(proof,lits,nll))){
 	if(!(res = push_into_resolvent(proof,lits,nll,expect_clause))){
 #endif
-	  std::cout << "extract theory lemma failed\n";
+	  // std::cout << "extract theory lemma failed\n";
           add_antes(proof);
 	  res = fix_lemma(lits,get_hyps(proof),nll);
 	}
@@ -1724,6 +1744,22 @@ public:
     frames = cnsts.size();
     traced_lit = ast();
   }
+
+  ~iz3translation_direct(){
+    for(hash_map<non_local_lits, non_local_lits *>::iterator
+	  it = non_local_lits_unique.begin(),
+	  en = non_local_lits_unique.end();
+	it != en;
+	++it)
+      delete it->second;
+
+    for(hash_map<Z3_resolvent, Z3_resolvent *>::iterator
+	  it = Z3_resolvent_unique.begin(),
+	  en = Z3_resolvent_unique.end();
+	it != en;
+	++it)
+      delete it->second;
+  }
 };
 
 
@@ -1740,29 +1776,29 @@ iz3translation *iz3translation::create(iz3mgr &mgr,
 }
 
 
-#if 0
+#if 1
 
-void iz3translation_direct_trace_lit(iz3translation_direct *p, ast lit, ast proof){
+void iz3translation_direct_trace_lit(iz3translation_direct *p, iz3mgr::ast lit, iz3mgr::ast proof){
    p->trace_lit(lit, proof);
 }
 
-void iz3translation_direct_show_step(iz3translation_direct *p,  ast proof){
+void iz3translation_direct_show_step(iz3translation_direct *p,  iz3mgr::ast proof){
    p->show_step(proof);
 }
 
-void iz3translation_direct_show_marked(iz3translation_direct *p,  ast proof){
+void iz3translation_direct_show_marked(iz3translation_direct *p,  iz3mgr::ast proof){
    p->show_marked(proof);
 }
 
-void iz3translation_direct_show_lit(iz3translation_direct *p,  ast lit){
+void iz3translation_direct_show_lit(iz3translation_direct *p,  iz3mgr::ast lit){
   p->show_lit(lit);
 }
 
-void iz3translation_direct_show_z3_lit(iz3translation_direct *p, ast a){
+void iz3translation_direct_show_z3_lit(iz3translation_direct *p, iz3mgr::ast a){
   p->show_z3_lit(a);
 }
 
-void iz3translation_direct_pfgoto(iz3translation_direct *p, ast proof){
+void iz3translation_direct_pfgoto(iz3translation_direct *p, iz3mgr::ast proof){
   p->pfgoto(proof);
 }
   
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index ef0b4ad6b..0e570321e 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -29,6 +29,7 @@ Revision History:
 #include"polynomial_cmds.h"
 #include"subpaving_cmds.h"
 #include"smt_strategic_solver.h"
+#include"smt_solver.h"
 
 extern bool g_display_statistics;
 extern void display_config();
@@ -96,6 +97,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
     cmd_context ctx;
 
     ctx.set_solver_factory(mk_smt_strategic_solver_factory());
+    ctx.set_interpolating_solver_factory(mk_smt_solver_factory());
 
     install_dl_cmds(ctx);
     install_dbg_cmds(ctx);