diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index b73f7a7a8..035cdd3c4 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1151,7 +1151,11 @@ class DotNetDLLComponent(Component):
                 out.write(' ')
                 out.write(cs_file)
             out.write('\n')
-            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name))
+            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name))
+            if DEBUG_MODE:
+                out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-')
+            else:
+                out.write(' /optimize+')
             if VS_X64:
                 out.write(' /platform:x64')
             else:
@@ -1174,6 +1178,13 @@ class DotNetDLLComponent(Component):
             mk_dir(os.path.join(dist_path, 'bin'))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                         '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
+                        '%s.xml' % os.path.join(dist_path, 'bin', self.dll_name))
+            if DEBUG_MODE:
+                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
+                            '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
+
+
 
     def mk_unix_dist(self, build_path, dist_path):
         # Do nothing
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 2c88a1978..03d5ff843 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -38,6 +38,7 @@ Revision History:
 #include"iz3hash.h"
 #include"iz3pp.h"
 #include"iz3checker.h"
+#include"scoped_proof.h"
 
 using namespace stl_ext;
 
@@ -290,6 +291,99 @@ extern "C" {
     opts->map[name] = value;
   }
 
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
+    Z3_TRY;
+    LOG_Z3_get_interpolant(c, pf, pat, p);
+    RESET_ERROR_CODE();
+
+    Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+    mk_c(c)->save_object(v);
+
+    ast *_pf = to_ast(pf);
+    ast *_pat = to_ast(pat);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    iz3interpolate(_m,
+		   _pf,
+		   cnsts,
+		   _pat,
+		   interp,
+		   (interpolation_options_struct *) 0 // ignore params for now
+		   );
+    
+    // copy result back
+    for(unsigned i = 0; i < interp.size(); i++){
+      v->m_ast_vector.push_back(interp[i]);
+      _m.dec_ref(interp[i]);
+    }
+    RETURN_Z3(of_ast_vector(v));
+    Z3_CATCH_RETURN(0);
+  }
+
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
+    Z3_TRY;
+    LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
+    RESET_ERROR_CODE();
+
+
+    // params_ref &_p = to_params(p)->m_params;
+    params_ref _p;
+    _p.set_bool("proof", true); // this is currently useless
+
+    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
+    scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
+    scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
+    m_solver.get()->updt_params(_p); // why do we have to do this?
+
+    ast *_pat = to_ast(pat);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    model_ref m;
+    lbool _status = iz3interpolate(_m,
+				   *(m_solver.get()),
+				   _pat,
+				   cnsts,
+				   interp,
+				   m,
+				   0 // ignore params for now
+				   );
+    
+    Z3_lbool status = of_lbool(_status);
+    
+    Z3_ast_vector_ref *v = 0;
+    *model = 0;
+
+    if(_status == l_false){
+      // copy result back
+      v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+      mk_c(c)->save_object(v);
+      for(unsigned i = 0; i < interp.size(); i++){
+	v->m_ast_vector.push_back(interp[i]);
+	_m.dec_ref(interp[i]);
+      }
+    }
+    else {
+      model_ref _m;
+      m_solver.get()->get_model(_m);
+      Z3_model_ref *crap = alloc(Z3_model_ref);
+      crap->m_model = _m.get();
+      mk_c(c)->save_object(crap);
+      *model = of_model(crap);
+    }
+
+    *out_interp = of_ast_vector(v);
+    
+    return status;
+    Z3_CATCH_RETURN(Z3_L_UNDEF);
+  }
 
 
 };
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index ac30a0c21..c8b1723f1 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -40,6 +40,7 @@ extern "C" {
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
+        s->m_solver->updt_params(p);
     }
 
     static void init_solver(Z3_context c, Z3_solver s) {
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 41ac1fa31..2b88cbab7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3523,7 +3523,7 @@ namespace Microsoft.Z3
         /// </summary>
         /// <remarks>
         /// The list of all configuration parameters can be obtained using the Z3 executable:
-        /// <c>z3.exe -ini?</c>
+        /// <c>z3.exe -p</c>
         /// Only a few configuration parameters are mutable once the context is created.
         /// An exception is thrown when trying to modify an immutable parameter.
         /// </remarks>
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal uint refCount = 0;
+        internal long refCount = 0;
 
         /// <summary>
         /// Finalizer.
diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs
index e8654ce21..8e474041a 100644
--- a/src/api/dotnet/Z3Object.cs
+++ b/src/api/dotnet/Z3Object.cs
@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Threading;
 
 namespace Microsoft.Z3
 {
@@ -50,8 +51,7 @@ namespace Microsoft.Z3
 
             if (m_ctx != null)
             {
-                m_ctx.refCount--;
-                if (m_ctx.refCount == 0)
+                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
                     GC.ReRegisterForFinalize(m_ctx);
                 m_ctx = null;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
@@ -85,7 +85,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
             IncRef(obj);
             m_n_obj = obj;
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index ce53a4c1f..50d29a790 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7253,3 +7253,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
+def Interp(a,ctx=None):
+    """Create an interpolation operator.
+    
+    The argument is an interpolation pattern (see tree_interpolant). 
+
+    >>> x = Int('x')
+    >>> print Interp(x>0)
+    interp(x > 0)
+    """
+    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
+    s = BoolSort(ctx)
+    a = s.cast(a)
+    return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+
+def tree_interpolant(pat,p=None,ctx=None):
+    """Compute interpolant for a tree of formulas.
+
+    The input is an interpolation pattern over a set of formulas C.
+    The pattern pat is a formula combining the formulas in C using
+    logical conjunction and the "interp" operator (see Interp). This
+    interp operator is logically the identity operator. It marks the
+    sub-formulas of the pattern for which interpolants should be
+    computed. The interpolant is a map sigma from marked subformulas
+    to formulas, such that, for each marked subformula phi of pat
+    (where phi sigma is phi with sigma(psi) substituted for each
+    subformula psi of phi such that psi in dom(sigma)):
+
+      1) phi sigma implies sigma(phi), and
+
+      2) sigma(phi) is in the common uninterpreted vocabulary between
+      the formulas of C occurring in phi and those not occurring in
+      phi
+
+      and moreover pat sigma implies false. In the simplest case
+      an interpolant for the pattern "(and (interp A) B)" maps A
+      to an interpolant for A /\ B. 
+
+      The return value is a vector of formulas representing sigma. This
+      vector contains sigma(phi) for each marked subformula of pat, in
+      pre-order traversal. This means that subformulas of phi occur before phi
+      in the vector. Also, subformulas that occur multiply in pat will
+      occur multiply in the result vector.
+
+    If pat is satisfiable, raises an object of class ModelRef
+    that represents a model of pat.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
+    [Not(x >= 0), Not(y <= 2)]
+
+    >>> g = And(Interp(x<0),x<2)
+    >>> try:
+    ...     print tree_interpolant(g).sexpr()
+    ... except ModelRef as m:
+    ...     print m.sexpr()
+    (define-fun x () Int
+      (- 1))
+    """
+    f = pat
+    ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
+    ptr = (AstVectorObj * 1)()
+    mptr = (Model * 1)()
+    if p == None:
+        p = ParamsRef(ctx)
+    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
+    if res == Z3_L_FALSE:
+        return AstVector(ptr[0],ctx)
+    raise ModelRef(mptr[0], ctx)
+
+def binary_interpolant(a,b,p=None,ctx=None):
+    """Compute an interpolant for a binary conjunction.
+
+    If a & b is unsatisfiable, returns an interpolant for a & b.
+    This is a formula phi such that
+
+    1) a implies phi
+    2) b implies not phi
+    3) All the uninterpreted symbols of phi occur in both a and b.
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a &b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> print binary_interpolant(x<0,x>2)
+    x <= 2
+    """
+    f = And(Interp(a),b)
+    return tree_interpolant(f,p,ctx)[0]
+
+def sequence_interpolant(v,p=None,ctx=None):
+    """Compute interpolant for a sequence of formulas.
+
+    If len(v) == N, and if the conjunction of the formulas in v is
+    unsatisfiable, the interpolant is a sequence of formulas w
+    such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
+
+    1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
+    2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
+    and v[i+1]..v[n]
+    
+    Requires len(v) >= 1. 
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a & b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print sequence_interpolant([x < 0, y == x , y > 2])
+    [Not(x >= 0), Not(y >= 0)]
+    """
+    f = v[0]
+    for i in range(1,len(v)):
+        f = And(Interp(f),v[i])
+    return tree_interpolant(f,p,ctx)
+
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index a26a958c0..593312d68 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -109,3 +109,4 @@ class FuncEntryObj(ctypes.c_void_p):
 class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
+
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 94e20eceb..b9f4975e8 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7699,6 +7699,108 @@ END_MLAPI_EXCLUDE
 
   Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
 
+  /** Compute an interpolant from a refutation. This takes a proof of
+      "false" from a set of formulas C, and an interpolation
+      pattern. The pattern pat is a formula combining the formulas in C
+      using logical conjunction and the "interp" operator (see
+      #Z3_mk_interp). This interp operator is logically the identity
+      operator. It marks the sub-formulas of the pattern for which interpolants should
+      be computed. The interpolant is a map sigma from marked subformulas to
+      formulas, such that, for each marked subformula phi of pat (where phi sigma
+      is phi with sigma(psi) substituted for each subformula psi of phi such that
+      psi in dom(sigma)):
+
+      1) phi sigma implies sigma(phi), and
+
+      2) sigma(phi) is in the common uninterpreted vocabulary between
+      the formulas of C occurring in phi and those not occurring in
+      phi
+
+      and moreover pat sigma implies false. In the simplest case
+      an interpolant for the pattern "(and (interp A) B)" maps A
+      to an interpolant for A /\ B. 
+
+      The return value is a vector of formulas representing sigma. The
+      vector contains sigma(phi) for each marked subformula of pat, in
+      pre-order traversal. This means that subformulas of phi occur before phi
+      in the vector. Also, subformulas that occur multiply in pat will
+      occur multiply in the result vector.
+
+      In particular, calling Z3_get_interpolant on a pattern of the
+      form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
+      result in a sequence interpolant for A_1, A_2,... A_N. 
+
+      Neglecting interp markers, the pattern must be a conjunction of
+      formulas in C, the set of premises of the proof. Otherwise an
+      error is flagged.
+
+      Any premises of the proof not present in the pattern are
+      treated as "background theory". Predicate and function symbols
+      occurring in the background theory are treated as interpreted and
+      thus always allowed in the interpolant.
+
+      Interpolant may not necessarily be computable from all
+      proofs. To be sure an interpolant can be computed, the proof
+      must be generated by an SMT solver for which interpoaltion is
+      supported, and the premises must be expressed using only
+      theories and operators for which interpolation is supported.
+
+      Currently, the only SMT solver that is supported is the legacy
+      SMT solver. Such a solver is available as the default solver in
+      #Z3_context objects produced by #Z3_mk_interpolation_context.
+      Currently, the theories supported are equality with
+      uninterpreted functions, linear integer arithmetic, and the
+      theory of arrays (in SMT-LIB terms, this is AUFLIA).
+      Quantifiers are allowed. Use of any other operators (including
+      "labels") may result in failure to compute an interpolant from a
+      proof.
+
+      Parameters:
+
+      \param c logical context.
+      \param pf a refutation from premises (assertions) C
+      \param pat an interpolation pattern over C
+      \param p parameters
+
+       def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
+    */
+
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
+
+  /* Compute an interpolant for an unsatisfiable conjunction of formulas.
+
+     This takes as an argument an interpolation pattern as in
+     #Z3_get_interpolant. This is a conjunction, some subformulas of
+     which are marked with the "interp" operator (see #Z3_mk_interp).
+     
+     The conjunction is first checked for unsatisfiability. The result
+     of this check is returned in the out parameter "status". If the result
+     is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
+     and returned as a vector of formulas. Otherwise the return value is
+     an empty formula. 
+
+     See #Z3_get_interpolant for a discussion of supported theories.
+
+     The advantage of this function over #Z3_get_interpolant is that
+     it is not necessary to create a suitable SMT solver and generate
+     a proof. The disadvantage is that it is not possible to use the
+     solver incrementally.
+
+     Parameters:
+     
+     \param c logical context.
+     \param pat an interpolation pattern
+     \param p parameters for solver creation
+     \param status returns the status of the sat check
+     \param model returns model if satisfiable
+
+     Return value: status of SAT check
+     
+     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
+  */
+  
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model);
+
 
 /** Constant reprepresenting a root of a formula tree for tree interpolation */
 #define IZ3_ROOT SHRT_MAX
diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index 1adedb2d7..df26422c8 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -106,7 +106,7 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
     return false;
 }
 
-bool float_decl_plugin::is_rm(expr * n, mpf_rounding_mode & val) {
+bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
     if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
         val = MPF_ROUND_NEAREST_TAWAY;
         return true;
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index 3786b76ee..58c37080d 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -169,7 +169,8 @@ public:
     app * mk_value(mpf const & v);
     bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); }
     bool is_value(expr * n, mpf & val);
-    bool is_rm(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); }
 
     mpf const & get_value(unsigned id) const { 
         SASSERT(m_value_table.contains(id));
@@ -198,7 +199,9 @@ public:
     sort * mk_float_sort(unsigned ebits, unsigned sbits);
     sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
     bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); }
-    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }    
+    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
+    bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
+    bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
     unsigned get_ebits(sort * s);
     unsigned get_sbits(sort * s);
 
@@ -217,8 +220,8 @@ public:
 
     app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
     bool is_value(expr * n) { return m_plugin->is_value(n); }
-    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }    
-    bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
+    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }     
+    bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
 
     app * mk_pzero(unsigned ebits, unsigned sbits);
     app * mk_nzero(unsigned ebits, unsigned sbits);
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 20925a0f9..d6f362902 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -28,9 +28,10 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m(m),
     m_simp(m),
     m_util(m),
-    m_mpf_manager(m_util.fm()),
-    m_mpz_manager(m_mpf_manager.mpz_manager()),
     m_bv_util(m),
+    m_arith_util(m),
+    m_mpf_manager(m_util.fm()),
+    m_mpz_manager(m_mpf_manager.mpz_manager()),    
     extra_assertions(m) {
     m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
 }
@@ -268,7 +269,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
         result = r;
     }
     else {
-        SASSERT(is_rm_sort(f->get_range()));
+        SASSERT(is_rm(f->get_range()));
 
         result = m.mk_fresh_const(
             #ifdef Z3DEBUG
@@ -281,6 +282,10 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
         m_rm_const2bv.insert(f, result);
         m.inc_ref(f);
         m.inc_ref(result);
+
+        expr_ref rcc(m);
+        rcc = bu().mk_ule(result, bu().mk_numeral(4, 3));
+        extra_assertions.push_back(rcc);
     }
 }
 
@@ -1847,6 +1852,55 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         // Just keep it here, as there will be something else that uses it.
         mk_triple(args[0], args[1], args[2], result);
     }
+    else if (num == 3 &&
+             m_bv_util.is_bv(args[0]) &&
+             m_arith_util.is_numeral(args[1]) &&
+             m_arith_util.is_numeral(args[2]))
+    {
+        // Three arguments, some of them are not numerals.
+        SASSERT(m_util.is_float(f->get_range()));
+        unsigned ebits = m_util.get_ebits(f->get_range());
+        unsigned sbits = m_util.get_sbits(f->get_range());
+
+        expr * rm = args[0];
+
+        rational q;
+        if (!m_arith_util.is_numeral(args[1], q))
+            NOT_IMPLEMENTED_YET();
+
+        rational e;
+        if (!m_arith_util.is_numeral(args[2], e))
+            NOT_IMPLEMENTED_YET();
+
+        SASSERT(e.is_int64());
+        SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
+
+        mpf nte, nta, tp, tn, tz;
+        m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator());
+
+        app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
+        a_nte = m_plugin->mk_value(nte);
+        a_nta = m_plugin->mk_value(nta);
+        a_tp = m_plugin->mk_value(tp);
+        a_tn = m_plugin->mk_value(tn);
+        a_tz = m_plugin->mk_value(tz);
+
+        expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
+        mk_value(a_nte->get_decl(), 0, 0, bv_nte);
+        mk_value(a_nta->get_decl(), 0, 0, bv_nta);
+        mk_value(a_tp->get_decl(), 0, 0, bv_tp);
+        mk_value(a_tn->get_decl(), 0, 0, bv_tn);
+        mk_value(a_tz->get_decl(), 0, 0, bv_tz);
+
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tn, bv_tz, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tp, result, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), bv_nta, result, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), bv_nte, result, result);        
+    }
     else if (num == 1 && m_bv_util.is_bv(args[0])) {
         sort * s = f->get_range();
         unsigned to_sbits = m_util.get_sbits(s);
@@ -1862,7 +1916,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
                   m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
                   result);
     }
-    else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {        
+    else if (num == 2 && 
+             is_app(args[1]) && 
+             m_util.is_float(m.get_sort(args[1]))) {        
         // We also support float to float conversion
         sort * s = f->get_range();
         expr_ref rm(m), x(m); 
@@ -2015,23 +2071,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
             mk_ite(c2, v2, result, result);
             mk_ite(c1, v1, result, result);
         }
-    }
-    else {
+    }    
+    else if (num == 2 &&              
+             m_util.is_rm(args[0]),
+             m_arith_util.is_real(args[1])) {
         // .. other than that, we only support rationals for asFloat
-        SASSERT(num == 2);
         SASSERT(m_util.is_float(f->get_range()));        
         unsigned ebits = m_util.get_ebits(f->get_range());
-        unsigned sbits = m_util.get_sbits(f->get_range());          
-        
-        SASSERT(m_bv_util.is_numeral(args[0]));        
-        rational tmp_rat; unsigned sz; 
-        m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);        
+        unsigned sbits = m_util.get_sbits(f->get_range());
+
+        SASSERT(m_bv_util.is_numeral(args[0]));
+        rational tmp_rat; unsigned sz;
+        m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
         SASSERT(tmp_rat.is_int32());
         SASSERT(sz == 3);
-        BV_RM_VAL bv_rm = (BV_RM_VAL) tmp_rat.get_unsigned();
-        
+        BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
+
         mpf_rounding_mode rm;
-        switch(bv_rm)
+        switch (bv_rm)
         {
         case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
         case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
@@ -2042,22 +2099,23 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         }
 
         SASSERT(m_util.au().is_numeral(args[1]));
-        
+
         rational q;
-        SASSERT(m_util.au().is_numeral(args[1]));
         m_util.au().is_numeral(args[1], q);
 
         mpf v;
         m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
-    
+
         expr * sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
-        expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits-1);
+        expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
         expr * e = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
 
         mk_triple(sgn, s, e, result);
 
         m_util.fm().del(v);
     }
+    else
+        UNREACHABLE();
 
     SASSERT(is_well_sorted(m, result));    
 }
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 2ccdac6a9..dcb508ffd 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -45,9 +45,10 @@ class fpa2bv_converter {
     ast_manager              & m;
     basic_simplifier_plugin    m_simp;
     float_util                 m_util;
+    bv_util                    m_bv_util;
+    arith_util                 m_arith_util;
     mpf_manager              & m_mpf_manager;
-    unsynch_mpz_manager      & m_mpz_manager;
-    bv_util                    m_bv_util;    
+    unsynch_mpz_manager      & m_mpz_manager;    
     float_decl_plugin        * m_plugin;
 
     obj_map<func_decl, expr*>  m_const2bv;
@@ -64,8 +65,9 @@ public:
 
     bool is_float(sort * s) { return m_util.is_float(s); }
     bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
+    bool is_rm(expr * e) { return m_util.is_rm(e); }
+    bool is_rm(sort * s) { return m_util.is_rm(s); }
     bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
-    bool is_rm_sort(sort * s) { return m_util.is_rm(s); }
 
     void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) {
         SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index b2e3da939..225aad668 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -78,17 +78,23 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             return BR_DONE;
         }
 
-        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
+        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
             m_conv.mk_rm_const(f, result);
             return BR_DONE;
         }
 
         if (m().is_eq(f)) {
             SASSERT(num == 2);
-            if (m_conv.is_float(args[0])) {
+            SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
+            sort * ds = f->get_domain()[0];
+            if (m_conv.is_float(ds)) {
                 m_conv.mk_eq(args[0], args[1], result);
                 return BR_DONE;
             }
+            else if (m_conv.is_rm(ds)) {
+                result = m().mk_eq(args[0], args[1]);
+                return BR_DONE;
+            }
             return BR_FAILED;
         }
 
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index ecd06ff38..a4212d579 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@@ -82,7 +82,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
     if (num_args == 2) {
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
         
         rational q;
@@ -109,12 +109,12 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
             return BR_FAILED;
     }
     else if (num_args == 3 && 
-             m_util.is_rm(m().get_sort(args[0])) && 
+             m_util.is_rm(args[0]) && 
              m_util.au().is_real(args[1]) &&
              m_util.au().is_int(args[2])) {
 
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
 
         rational q;
@@ -129,8 +129,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
         mpf v;
 	    m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
         result = m_util.mk_value(v);
-        m_util.fm().del(v);        
-        // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
+        m_util.fm().del(v);
         return BR_DONE;
     }
     else {
@@ -140,7 +139,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
 br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -161,7 +160,7 @@ br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -176,7 +175,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -287,7 +286,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
             scoped_mpf t(m_util.fm());
@@ -302,7 +301,7 @@ br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, exp
 
 br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());
@@ -317,7 +316,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 527230e16..836ade9ce 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -547,6 +547,9 @@ public:
     }
 };
 
+#define STRINGIZE(x) #x
+#define STRINGIZE_VALUE_OF(x) STRINGIZE(x)
+
 class get_info_cmd : public cmd {
     symbol   m_error_behavior;
     symbol   m_name;
@@ -584,7 +587,11 @@ public:
             ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl;
         }
         else if (opt == m_version) {
-            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl;
+            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
+#ifdef Z3GITHASH
+                << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH)
+#endif
+                << "\")" << std::endl;
         }
         else if (opt == m_status) {
             ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;
diff --git a/src/duality/duality.h b/src/duality/duality.h
index c315c5431..c1c9797f3 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1152,6 +1152,13 @@ protected:
 
       virtual void LearnFrom(Solver *old_solver) = 0;
 
+      /** Return true if the solution be incorrect due to recursion bounding.
+	  That is, the returned "solution" might contain all derivable facts up to the
+	  given recursion bound, but not be actually a fixed point.
+       */
+
+      virtual bool IsResultRecursionBounded() = 0;
+
       virtual ~Solver(){}
 
       static Solver *Create(const std::string &solver_class, RPFP *rpfp);
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 59611c814..681582415 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -768,6 +768,29 @@ namespace Duality {
       annot.Simplify();
     }    
 
+    bool recursionBounded;
+
+    /** See if the solution might be bounded. */
+    void TestRecursionBounded(){
+      recursionBounded = false;
+      if(RecursionBound == -1)
+	return;
+      for(unsigned i = 0; i < nodes.size(); i++){
+	Node *node = nodes[i];
+	std::vector<Node *> &insts = insts_of_node[node];
+	for(unsigned j = 0; j < insts.size(); j++)
+	  if(indset->Contains(insts[j]))
+	    if(NodePastRecursionBound(insts[j])){
+	      recursionBounded = true;
+	      return;
+	    }
+      }
+    }    
+
+    bool IsResultRecursionBounded(){
+      return recursionBounded;
+    }
+
     /** Generate a proposed solution of the input RPFP from
 	the unwinding, by unioning the instances of each node. */
     void GenSolutionFromIndSet(bool with_markers = false){
@@ -1026,6 +1049,7 @@ namespace Duality {
 	timer_stop("ProduceCandidatesForExtension");
 	if(candidates.empty()){
 	  GenSolutionFromIndSet();
+	  TestRecursionBounded();
 	  return true;
 	}
 	Candidate cand = candidates.front();
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index bed93a56f..0d394090f 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -41,6 +41,7 @@ Revision History:
 #include "iz3hash.h"
 #include "iz3interp.h"
 
+#include"scoped_proof.h"
 
 
 using namespace stl_ext;
@@ -347,8 +348,10 @@ public:
     // 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();
+    for(unsigned i = 0; i < pos_map.size(); i++){
+      unsigned j = pos_map[i];
+      interps[i] = j < _interps.size() ? _interps[j] : mk_false();
+    }
   }
 
   bool has_interp(hash_map<ast,bool> &memo, const ast &t){
@@ -501,6 +504,8 @@ lbool iz3interpolate(ast_manager &_m_manager,
   return res;
 }
 
+
+
 void interpolation_options_struct::apply(iz3base &b){
   for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
       it != en;
diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h
index 52aa716c3..1c6f9513e 100644
--- a/src/interp/iz3interp.h
+++ b/src/interp/iz3interp.h
@@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager,
 		    ptr_vector<ast> &interps,
 		    interpolation_options_struct * options);
 
+
 /* Compute an interpolant from an ast representing an interpolation
    problem, if unsat, else return a model (if enabled). Uses the
    given solver to produce the proof/model. Also returns a vector
@@ -90,4 +91,5 @@ lbool iz3interpolate(ast_manager &_m_manager,
 		     model_ref &m,
 		     interpolation_options_struct * options);
 
+
 #endif
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 1952cc42f..7349fa889 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -53,6 +53,7 @@ namespace datalog {
         MEMOUT,
         INPUT_ERROR,
         APPROX,
+	BOUNDED,
         CANCELED
     };
 
@@ -304,6 +305,8 @@ namespace datalog {
            \brief Retrieve predicates
         */
         func_decl_set const& get_predicates() const { return m_preds; }
+	ast_ref_vector const &get_pinned() const {return m_pinned; }
+
         bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); }
         bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); }
 
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 0584e6b58..849cf94ea 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -36,6 +36,7 @@ Revision History:
 #include "model_v2_pp.h"
 #include "fixedpoint_params.hpp"
 #include "used_vars.h"
+#include "func_decl_dependencies.h"
 
 // template class symbol_table<family_id>;
 
@@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) {
     _d->rpfp->AssertAxiom(e);
   }
   
+  // make sure each predicate is the head of at least one clause
+  func_decl_set heads;
+  for(unsigned i = 0; i < clauses.size(); i++){
+    expr cl = clauses[i];
+
+    while(true){
+      if(cl.is_app()){
+	decl_kind k = cl.decl().get_decl_kind();
+	if(k == Implies)
+	  cl = cl.arg(1);
+	else {
+	  heads.insert(cl.decl());
+	  break;
+	}
+      }
+      else if(cl.is_quantifier())
+	cl = cl.body();
+      else break;
+    }
+  }
+  ast_ref_vector const &pinned = m_ctx.get_pinned();
+  for(unsigned i = 0; i < pinned.size(); i++){
+    ::ast *fa = pinned[i];
+    if(is_func_decl(fa)){
+      ::func_decl *fd = to_func_decl(fa);
+      if(m_ctx.is_predicate(fd)) {
+	func_decl f(_d->ctx,fd);
+	if(!heads.contains(fd)){
+	  int arity = f.arity();
+	  std::vector<expr> args;
+	  for(int j = 0; j < arity; j++)
+	    args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
+	  expr c = implies(_d->ctx.bool_val(false),f(args));
+	  c = _d->ctx.make_quant(Forall,args,c);
+	  clauses.push_back(c);
+	}
+      }
+    }
+  }
+
   // creates 1-1 map between clauses and rpfp edges
   _d->rpfp->FromClauses(clauses);
 
@@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) {
   // dealloc(rs); this is now owned by data
 
   // true means the RPFP problem is SAT, so the query is UNSAT
-  return ans ? l_false : l_true;
+  // but we return undef if the UNSAT result is bounded
+  if(ans){
+    if(rs->IsResultRecursionBounded()){
+#if 0
+      m_ctx.set_status(datalog::BOUNDED);
+      return l_undef;
+#else
+      return l_false;
+#endif
+    }
+    return l_false;
+  }
+  return l_true;
 }
 
 expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 827b90e60..f9916808c 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -252,6 +252,11 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
+	    if(dlctx.get_status() == datalog::BOUNDED){
+	      ctx.regular_stream() << "bounded\n";
+	      print_certificate(ctx);
+	      break;
+	    }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {
             case datalog::INPUT_ERROR:
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index b09280d35..94dd5d0a0 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -736,6 +736,11 @@ namespace pdr {
         m_closed = true; 
     }
 
+    void model_node::reopen() {
+        SASSERT(m_closed);
+        m_closed = false;
+    }
+
     static bool is_ini(datalog::rule const& r) {
         return r.get_uninterpreted_tail_size() == 0;
     }
@@ -745,6 +750,7 @@ namespace pdr {
             return const_cast<datalog::rule*>(m_rule);
         }
         // only initial states are not set by the PDR search.
+        SASSERT(m_model.get());
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -864,9 +870,10 @@ namespace pdr {
     }
 
     void model_search::add_leaf(model_node& n) {
-        unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
-        ++count;
-        if (count == 1 || is_repeated(n)) {
+        model_nodes ns;
+        model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
+        nodes.push_back(&n);
+        if (nodes.size() == 1 || is_repeated(n)) {
             set_leaf(n);
         }
         else {
@@ -875,7 +882,7 @@ namespace pdr {
     }
 
     void model_search::set_leaf(model_node& n) {
-        erase_children(n);
+        erase_children(n, true);
         SASSERT(n.is_open());      
         enqueue_leaf(n);
     }
@@ -897,7 +904,7 @@ namespace pdr {
         set_leaf(*root);
     }
 
-    obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
+    obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
         unsigned l = n.orig_level();
         if (l >= m_cache.size()) {
             m_cache.resize(l + 1);
@@ -905,7 +912,7 @@ namespace pdr {
         return m_cache[l];
     }
 
-    void model_search::erase_children(model_node& n) {
+    void model_search::erase_children(model_node& n, bool backtrack) {
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
         erase_leaf(n);
@@ -916,13 +923,20 @@ namespace pdr {
             nodes.push_back(m);
             todo.append(m->children());
             erase_leaf(*m);
-            remove_node(*m);
+            remove_node(*m, backtrack);
         }
         std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
     }
 
-    void model_search::remove_node(model_node& n) {
-        if (0 == --cache(n).find(n.state())) {
+    void model_search::remove_node(model_node& n, bool backtrack) {
+        model_nodes& nodes = cache(n).find(n.state());
+        nodes.erase(&n);
+        if (nodes.size() > 0 && n.is_open() && backtrack) {
+            for (unsigned i = 0; i < nodes.size(); ++i) {
+                nodes[i]->reopen();
+            }
+        }
+        if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
     }
@@ -1203,8 +1217,8 @@ namespace pdr {
 
     void model_search::reset() {
         if (m_root) {
-            erase_children(*m_root);
-            remove_node(*m_root);
+            erase_children(*m_root, false);
+            remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
         }
@@ -1240,7 +1254,7 @@ namespace pdr {
           m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
-          m_search(m_params.bfs_model_search()),
+          m_search(m_params.bfs_model_search(), m),
           m_last_result(l_undef),
           m_inductive_lvl(0),
           m_expanded_lvl(0),
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 8a4f3e438..a85011600 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -231,6 +231,7 @@ namespace pdr {
         }
 
         void set_closed();     
+        void reopen();
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
@@ -243,19 +244,21 @@ namespace pdr {
     };
 
     class model_search {
+        typedef ptr_vector<model_node> model_nodes;
+        ast_manager&       m;
         bool               m_bfs;
         model_node*        m_root;
         std::deque<model_node*> m_leaves;
-        vector<obj_map<expr, unsigned> > m_cache;
+        vector<obj_map<expr, model_nodes > > m_cache;
         
-        obj_map<expr, unsigned>& cache(model_node const& n);
-        void erase_children(model_node& n);
+        obj_map<expr, model_nodes>& cache(model_node const& n);
+        void erase_children(model_node& n, bool backtrack);
         void erase_leaf(model_node& n);
-        void remove_node(model_node& n);
+        void remove_node(model_node& n, bool backtrack);
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
         void update_models();
     public:
-        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
         ~model_search();
 
         void reset();
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e7037f31a..998dd72e6 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -85,6 +85,7 @@ namespace smt {
         typedef typename Ext::numeral     numeral;
         typedef typename Ext::inf_numeral inf_numeral;
         typedef vector<numeral> numeral_vector; 
+        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
 
         static const int    dead_row_id = -1;
     protected:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 195d78e25..fbc043048 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2780,7 +2780,6 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::refine_epsilon() {
-        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
         while (true) {
             rational2var mapping;
             theory_var num = get_num_vars();
@@ -2788,6 +2787,8 @@ namespace smt {
             for (theory_var v = 0; v < num; v++) {
                 if (is_int(v))
                     continue;
+                if (!get_context().is_shared(get_enode(v)))
+                    continue;
                 inf_numeral const & val = get_value(v);
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index bab921ed2..d02c9e540 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -654,6 +654,7 @@ namespace smt {
         }
         return get_value(v, computed_epsilon) == val;
     }
+    
 
     /**
        \brief Return true if for every monomial x_1 * ... * x_n,
@@ -2309,8 +2310,9 @@ namespace smt {
         if (m_nl_monomials.empty())
             return FC_DONE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return FC_DONE;
+        }
 
         if (!m_params.m_nl_arith)
             return FC_GIVEUP;
@@ -2338,9 +2340,10 @@ namespace smt {
         if (!max_min_nl_vars())
             return FC_CONTINUE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
-        
+        }
+
         svector<theory_var> vars;
         get_non_linear_cluster(vars);
 
@@ -2391,8 +2394,9 @@ namespace smt {
         }
         while (m_nl_strategy_idx != old_idx);
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
+        }
 
         TRACE("non_linear", display(tout););
 
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 603898af8..8ff5f8e8f 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -165,6 +165,14 @@ public:
         SASSERT(e);
         return e->get_data().m_value;
     }
+
+    value const & operator[](key * k) const {
+        return find(k);
+    }
+
+    value & operator[](key * k) {
+        return find(k);
+    }
     
     iterator find_iterator(Key * k) const { 
         return m_table.find(key_data(k));