Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt

2025-04-10 19:27:06 +00:00 · 2014-02-11 15:44:12 -08:00 · 2014-02-11 15:44:12 -08:00 · c42ee3bb01
parent 480ec049c0 f45ad4bdc0
commit c42ee3bb01
37 changed files with 2162 additions and 182 deletions
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@ -638,7 +638,13 @@ def is_compiler(given, expected):
 def is_CXX_gpp():
    return is_compiler(CXX, 'g++')

+def is_clang_in_gpp_form(cc):
+    version_string = subprocess.check_output([cc, '--version'])
+    return version_string.find('clang') != -1
+
 def is_CXX_clangpp():
+    if is_compiler(CXX, 'g++'):
+        return is_clang_in_gpp_form(CXX)
    return is_compiler(CXX, 'clang++')

 def get_cpp_files(path):
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@ -17,6 +17,7 @@ Revision History:
 --*/
 #include<iostream>
 #include<sstream>
+#include<vector>
 #include"z3.h"
 #include"api_log_macros.h"
 #include"api_context.h"
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort

 void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
    ast_manager& m = const_cast<ast_manager&>(*this);
+
    if (decl->is_associative()) {
        sort * expected = decl->get_domain(0);
        for (unsigned i = 0; i < num_args; i++) {
@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const {
    if  (n->get_kind() != AST_APP) 
        return; // nothing else to check...
    app const * a = to_app(n);
-    check_sort(a->get_decl(), a->get_num_args(), a->get_args());
+    func_decl* d = a->get_decl();
+    check_sort(d, a->get_num_args(), a->get_args());
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_right_associative()) {
+        check_sorts_core(a->get_arg(1));
+    }
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_left_associative()) {
+        check_sorts_core(a->get_arg(0));
+    }
 }

 bool ast_manager::check_sorts(ast const * n) const {
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
    if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {
        s = to_sort(parameters[0].get_ast());
    }
+    else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) {
+        s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+    }
    else if (range != 0 && is_float_sort(range)) {
        s = range;
    }
@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
        sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
        symbol name("asFloat");
        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
-    }    
+    }
+    else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
+        if (num_parameters != 2)
+            m_manager->raise_exception("invalid number of parameters to to_fp");
+        if (!parameters[0].is_int() || !parameters[1].is_int())
+            m_manager->raise_exception("invalid parameter type to to_fp");
+        int ebits = parameters[0].get_int();
+        int sbits = parameters[1].get_int();
+        
+        sort * fp = mk_float_sort(ebits, sbits);
+        symbol name("asFloat");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
    else {
        // .. Otherwise we only know how to convert rationals/reals. 
        if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) 
@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter
    return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));        
 }

+func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                          unsigned arity, sort * const * domain, sort * range) {
+    if (!m_bv_plugin)
+        m_manager->raise_exception("fp unsupported; use a logic with BV support");
+    if (arity != 3)
+        m_manager->raise_exception("invalid number of arguments to fp");    
+    if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
+        !is_sort_of(domain[1], m_bv_fid, BV_SORT) ||
+        !is_sort_of(domain[2], m_bv_fid, BV_SORT))
+        m_manager->raise_exception("sort mismtach");
+        
+    sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1);
+    symbol name("fp");
+    return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
+}
+
+func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                                 unsigned arity, sort * const * domain, sort * range) {
+    if (!m_bv_plugin)
+        m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support");
+    if (arity != 2)
+        m_manager->raise_exception("invalid number of arguments to to_fp_unsigned");
+    if (is_rm_sort(domain[0]))
+        m_manager->raise_exception("sort mismtach");
+    if (!is_sort_of(domain[1], m_bv_fid, BV_SORT))
+        m_manager->raise_exception("sort mismtach");
+
+    sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+    symbol name("to_fp_unsigned");
+    return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
+}
+
+func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
+func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
+func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
 func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                            unsigned arity, sort * const * domain, sort * range) {
    switch (k) {
@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
        return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
    case OP_TO_IEEE_BV:
        return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_FP:
+        return mk_from3bv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_FP_UNSIGNED:
+        return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_UBV:
+        return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_SBV:
+        return mk_to_sbv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_REAL:
+        return mk_to_real(k, num_parameters, parameters, arity, domain, range);
    default:
        m_manager->raise_exception("unsupported floating point operator");
        return 0;
@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
    if (m_bv_plugin)
        op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));

-    // We also support draft version 3
-    op_names.push_back(builtin_name("fp", OP_TO_FLOAT));
+    // These are the operators from the final draft of the SMT FloatingPoints standard
+    op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
+    op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));

    op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
    op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
    op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
    op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
    op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
-    op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT));
+    op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));

    if (m_bv_plugin) {
-    // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT));
-    // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT));
-    // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT));
-    // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV));
-    // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV));
+        op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
+        op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
+        op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
+        op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
    }
-    
-    op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT));
+        
    // op_names.push_back(builtin_name("fp.toReal", ?));
 }

 void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
    sort_names.push_back(builtin_name("FP", FLOAT_SORT));
    sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
+
+    // In the SMT FPA final draft, FP is called FloatingPoint
+    sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
 }

 expr * float_decl_plugin::get_some_value(sort * s) {
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@ -72,6 +72,12 @@ enum float_op_kind {

    OP_TO_FLOAT,
    OP_TO_IEEE_BV,
+
+    OP_FLOAT_FP,
+    OP_FLOAT_TO_FP_UNSIGNED,
+    OP_FLOAT_TO_UBV,
+    OP_FLOAT_TO_SBV,
+    OP_FLOAT_TO_REAL,
    
    LAST_FLOAT_OP
 };
@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin {
                            unsigned arity, sort * const * domain, sort * range);
    func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                              unsigned arity, sort * const * domain, sort * range);
-
+    func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                           unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                  unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                             unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                             unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                              unsigned arity, sort * const * domain, sort * range);
+    
    virtual void set_manager(ast_manager * m, family_id id);
    unsigned mk_id(mpf const & v);
    void recycled_id(unsigned id);
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
    case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
    case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
    case OP_TO_IEEE_BV:      SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
+    case OP_FLOAT_FP:        SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break;
+    case OP_FLOAT_TO_UBV:    SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break;
+    case OP_FLOAT_TO_SBV:    SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break;
+    case OP_FLOAT_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
    }
    return st;
 }
@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
 br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
    return BR_FAILED;
 }
+
+br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+    bv_util bu(m());
+    rational r1, r2, r3;
+    unsigned bvs1, bvs2, bvs3;
+
+    if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) {        
+        SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator()));
+        SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator()));
+        SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator()));
+        scoped_mpf v(m_util.fm());
+        mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator());
+        m_util.fm().set(v, bvs2, bvs3 + 1,
+                        r1.is_one(),
+                        r3.to_mpq().numerator(),
+                        m_util.fm().unbias_exp(bvs2, biased_exp));
+        TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;);
+        result = m_util.mk_value(v);
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) {
+    return BR_FAILED;
+}
--- a/src/ast/rewriter/float_rewriter.h
+++ b/src/ast/rewriter/float_rewriter.h
@ -73,6 +73,12 @@ public:
    br_status mk_is_sign_minus(expr * arg1, expr_ref & result);

    br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
+
+    br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_real(expr * arg1, expr_ref & result);
 };

 #endif
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_

  ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
  ptr_vector<expr>::const_iterator end = ctx.end_assertions();
-  ptr_vector<ast> cnsts(end - it);
+  ptr_vector<ast> cnsts((unsigned)(end - it));
  for (int i = 0; it != end; ++it, ++i)
  cnsts[i] = *it;
    
@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
  get_interpolant_and_maybe_check(ctx,t,m_params,false);
 }

+#if 0
 static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
  get_interpolant_and_maybe_check(ctx,t,m_params,true);
 }
-
+#endif

 static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
    
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@ -36,12 +36,11 @@ namespace Duality {
  struct Z3User {

      context &ctx;
-      solver &slvr;

      typedef func_decl FuncDecl;
      typedef expr Term;

-      Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){}
+      Z3User(context &_ctx) : ctx(_ctx){}
  
      const char *string_of_int(int n);
      
@ -53,6 +52,8 @@ namespace Duality {

      Term SubstRec(hash_map<ast, Term> &memo, const Term &t);

+      Term SubstRec(hash_map<ast, Term> &memo, hash_map<func_decl, func_decl> &map, const Term &t);
+
      void Strengthen(Term &x, const Term &y);

        // return the func_del of an app if it is uninterpreted
@ -77,14 +78,14 @@ namespace Duality {

      void Summarize(const Term &t);

-      int CumulativeDecisions();
-
      int CountOperators(const Term &t);

      Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);

      Term RemoveRedundancy(const Term &t);

+      Term IneqToEq(const Term &t);
+
      bool IsLiteral(const expr &lit, expr &atom, expr &val);

      expr Negate(const expr &f);
@ -98,7 +99,10 @@ namespace Duality {
      bool IsClosedFormula(const Term &t);

      Term AdjustQuantifiers(const Term &t);
-private:
+
+      FuncDecl RenumberPred(const FuncDecl &f, int n);
+
+protected:

      void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
      int CountOperatorsRec(hash_set<ast> &memo, const Term &t);
@ -108,6 +112,7 @@ private:
      expr ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res);
      expr FinishAndOr(const std::vector<expr> &args, bool is_and);
      expr PullCommonFactors(std::vector<expr> &args, bool is_and);
+      Term IneqToEqRec(hash_map<ast, Term> &memo, const Term &t);


 };
@ -256,9 +261,9 @@ private:
        }
 #endif

-      iZ3LogicSolver(context &c) : LogicSolver(c) {
+      iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) {
          ctx = ictx = &c;
-          slvr = islvr = new interpolating_solver(*ictx);
+          slvr = islvr = new interpolating_solver(*ictx, models);
          need_goals = false;
          islvr->SetWeakInterpolants(true);
        }
@ -308,8 +313,8 @@ private:
      }

      LogicSolver *ls;
-        
-    private:
+
+    protected:
      int nodeCount;
      int edgeCount;
      
@ -324,7 +329,7 @@ private:
      
    public:
      model dualModel;
-    private:
+    protected:
      literals dualLabels;
      std::list<stack_entry> stack;
      std::vector<Term> axioms; // only saved here for printing purposes
@ -340,7 +345,7 @@ private:
 	  inherit the axioms. 
      */

-    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
+    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
      {
        ls = _ls;
 	nodeCount = 0;
@ -350,7 +355,7 @@ private:
 	proof_core = 0;
      }

-      ~RPFP();
+      virtual ~RPFP();
      
      /** Symbolic representation of a relational transformer */
      class Transformer
@ -574,7 +579,7 @@ private:
       * you must pop the context accordingly. The second argument is
       * the number of pushes we are inside. */
      
-      void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
+      virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);

      /* Constrain an edge by the annotation of one of its children. */

@ -808,9 +813,31 @@ private:
       /** Edges of the graph. */
       std::vector<Edge *> edges;

+       /** Fuse a vector of transformers. If the total number of inputs of the transformers
+	   is N, then the result is an N-ary transfomer whose output is the union of
+	   the outputs of the given transformers. The is, suppose we have a vetor of transfoermers
+	   {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer 
+	       
+	       F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = 
+	           T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M))
+       */
+
+      Transformer Fuse(const std::vector<Transformer *> &trs);
+
+      /** Fuse edges so that each node is the output of at most one edge. This
+	  transformation is solution-preserving, but changes the numbering of edges in
+	  counterexamples.
+      */
+      void FuseEdges();
+
+      void RemoveDeadNodes();
+
      Term SubstParams(const std::vector<Term> &from,
 		       const std::vector<Term> &to, const Term &t);

+      Term SubstParamsNoCapture(const std::vector<Term> &from,
+				const std::vector<Term> &to, const Term &t);
+
      Term Localize(Edge *e, const Term &t);

      void EvalNodeAsConstraint(Node *p, Transformer &res);
@ -829,7 +856,13 @@ private:
       */
      void ComputeProofCore();

-    private:
+      int CumulativeDecisions();
+
+      solver &slvr(){
+	return *ls->slvr;
+      }
+
+    protected:
      
      void ClearProofCore(){
 	if(proof_core)
@ -947,6 +980,8 @@ private:

      expr SimplifyOr(std::vector<expr> &lits);

+      expr SimplifyAnd(std::vector<expr> &lits);
+
      void SetAnnotation(Node *root, const expr &t);

      void AddEdgeToSolver(Edge *edge);
@ -959,9 +994,58 @@ private:
    
      expr NegateLit(const expr &f);

+      expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox);
+
+      bool IsVar(const expr &t);
+
+      void GetVarsRec(hash_set<ast> &memo, const expr &cnst, std::vector<expr> &vars);
+
+      expr UnhoistPullRec(hash_map<ast,expr> & memo, const expr &w, hash_map<ast,expr> & init_defs, hash_map<ast,expr> & const_params, hash_map<ast,expr> &const_params_inv, std::vector<expr> &new_params);
+
+      void AddParamsToTransformer(Transformer &trans, const std::vector<expr> &params);
+ 
+      expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector<expr> &params);
+
+      expr GetRelRec(hash_set<ast> &memo, const expr &t, const func_decl &rel);
+
+      expr GetRel(Edge *edge, int child_idx);
+
+      void GetDefs(const expr &cnst, hash_map<ast,expr> &defs);
+
+      void GetDefsRec(const expr &cnst, hash_map<ast,expr> &defs);
+
+      void AddParamsToNode(Node *node, const std::vector<expr> &params);
+
+      void UnhoistLoop(Edge *loop_edge, Edge *init_edge);
+
+      void Unhoist();
+      
+      Term ElimIteRec(hash_map<ast,expr> &memo, const Term &t, std::vector<expr> &cnsts);
+
+      Term ElimIte(const Term &t);
+
+      void MarkLiveNodes(hash_map<Node *,std::vector<Edge *> > &outgoing, hash_set<Node *> &live_nodes, Node *node);
+
+      virtual void slvr_add(const expr &e);
+      
+      virtual void slvr_pop(int i);
+
+      virtual void slvr_push();
+      
+      virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0);
+
+      virtual lbool ls_interpolate_tree(TermTree *assumptions,
+					TermTree *&interpolants,
+					model &_model,
+					TermTree *goals = 0,
+					bool weak = false);
+
+      virtual bool proof_core_contains(const expr &e);
+
    };
    
-    /** RPFP solver base class. */
+
+  /** RPFP solver base class. */

    class Solver {
      
@ -1005,6 +1089,8 @@ private:
      /** Object thrown on cancellation */
      struct Canceled {};
      
+      /** Object thrown on incompleteness */
+      struct Incompleteness {};
    };
 }

@ -1042,3 +1128,130 @@ namespace std {
    }
  };
 }
+
+// #define LIMIT_STACK_WEIGHT 5
+
+
+namespace Duality {
+    /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */
+
+    class RPFP_caching : public RPFP {
+  public:
+
+      /** appends assumption literals for edge to lits. if with_children is true,
+	  includes that annotation of the edge's children. 
+       */ 
+      void AssertEdgeCache(Edge *e, std::vector<Term> &lits, bool with_children = false);
+      
+      /** appends assumption literals for node to lits */
+      void AssertNodeCache(Node *, std::vector<Term> lits);
+
+      /** check assumption lits, and return core */
+      check_result CheckCore(const std::vector<Term> &assumps, std::vector<Term> &core);
+      
+      /** Clone another RPFP into this one, keeping a map */
+      void Clone(RPFP *other);
+
+      /** Get the clone of a node */
+      Node *GetNodeClone(Node *other_node);
+
+      /** Get the clone of an edge */
+      Edge *GetEdgeClone(Edge *other_edge);
+
+      /** Try to strengthen the parent of an edge */
+      void GeneralizeCache(Edge *edge);
+
+      /** Try to propagate some facts from children to parents of edge.
+	  Return true if success. */
+      bool PropagateCache(Edge *edge);
+
+      /** Construct a caching RPFP using a LogicSolver */
+      RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {}
+
+      /** Constraint an edge by its child's annotation. Return
+	  assumption lits. */
+      void ConstrainParentCache(Edge *parent, Node *child, std::vector<Term> &lits);
+
+#ifdef LIMIT_STACK_WEIGHT
+      virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
+#endif
+
+      virtual ~RPFP_caching(){}
+
+  protected:
+      hash_map<ast,expr> AssumptionLits;
+      hash_map<Node *, Node *> NodeCloneMap;
+      hash_map<Edge *, Edge *> EdgeCloneMap;
+      std::vector<expr> alit_stack;
+      std::vector<unsigned> alit_stack_sizes;
+      hash_map<Edge *, uptr<LogicSolver> > edge_solvers;
+      
+#ifdef LIMIT_STACK_WEIGHT
+      struct weight_counter {
+	int val;
+	weight_counter(){val = 0;}
+	void swap(weight_counter &other){
+	  std::swap(val,other.val);
+	}
+      };
+      
+      struct big_stack_entry {
+	weight_counter weight_added;
+	std::vector<expr> new_alits;
+	std::vector<expr> alit_stack;
+	std::vector<unsigned> alit_stack_sizes;
+      };
+
+      std::vector<expr> new_alits;
+      weight_counter weight_added;
+      std::vector<big_stack_entry> big_stack;
+#endif
+
+
+
+      void GetAssumptionLits(const expr &fmla, std::vector<expr> &lits, hash_map<ast,expr> *opt_map = 0);
+
+      void GreedyReduceCache(std::vector<expr> &assumps, std::vector<expr> &core);
+
+      void FilterCore(std::vector<expr> &core, std::vector<expr> &full_core);
+      void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector<expr> &lits);
+
+      virtual void slvr_add(const expr &e);
+      
+      virtual void slvr_pop(int i);
+
+      virtual void slvr_push();
+      
+      virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0);
+
+      virtual lbool ls_interpolate_tree(TermTree *assumptions,
+					TermTree *&interpolants,
+					model &_model,
+					TermTree *goals = 0,
+					bool weak = false);
+
+      virtual bool proof_core_contains(const expr &e);
+
+      void GetTermTreeAssertionLiterals(TermTree *assumptions);
+
+      void GetTermTreeAssertionLiteralsRec(TermTree *assumptions);
+
+      LogicSolver *SolverForEdge(Edge *edge, bool models);
+
+  public:
+      struct scoped_solver_for_edge {
+	LogicSolver *orig_ls;
+	RPFP_caching *rpfp;
+	scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){
+	  rpfp = _rpfp;
+	  orig_ls = rpfp->ls;
+	  rpfp->ls = rpfp->SolverForEdge(edge,models);
+	}
+	~scoped_solver_for_edge(){
+	  rpfp->ls = orig_ls;
+	}
+      };
+
+    };
+
+}
--- a/src/duality/duality_profiling.cpp
+++ b/src/duality/duality_profiling.cpp
@ -25,7 +25,14 @@ Revision History:
 #include <string.h>
 #include <stdlib.h>

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
 #include "duality_wrapper.h"
+#include "iz3profiling.h"

 namespace Duality {
  
@ -103,6 +110,7 @@ namespace Duality {
      output_time(*pfs, it->second.t);
      (*pfs) << std::endl;
    }
+    profiling::print(os); // print the interpolation stats
  }
  
  void timer_start(const char *name){
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@ -19,6 +19,12 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
 #include "duality.h"
 #include "duality_profiling.h"

@ -26,6 +32,7 @@ Revision History:
 #include <set>
 #include <map>
 #include <list>
+#include <iterator>

 // TODO: make these official options or get rid of them

@ -37,14 +44,18 @@ Revision History:
 #define MINIMIZE_CANDIDATES
 // #define MINIMIZE_CANDIDATES_HARDER
 #define BOUNDED
-#define CHECK_CANDS_FROM_IND_SET
+// #define CHECK_CANDS_FROM_IND_SET
 #define UNDERAPPROX_NODES
 #define NEW_EXPAND
 #define EARLY_EXPAND
 // #define TOP_DOWN
 // #define EFFORT_BOUNDED_STRAT
 #define SKIP_UNDERAPPROX_NODES
-
+#define USE_RPFP_CLONE
+// #define KEEP_EXPANSIONS
+// #define USE_CACHING_RPFP
+// #define PROPAGATE_BEFORE_CHECK
+#define USE_NEW_GEN_CANDS

 namespace Duality {

@ -101,7 +112,7 @@ namespace Duality {
  public:
    Duality(RPFP *_rpfp)
      : ctx(_rpfp->ctx),
-	slvr(_rpfp->slvr),
+	slvr(_rpfp->slvr()),
        nodes(_rpfp->nodes),
        edges(_rpfp->edges)
    {
@ -115,8 +126,42 @@ namespace Duality {
      Report = false;
      StratifiedInlining = false;
      RecursionBound = -1;
+      {
+	scoped_no_proof no_proofs_please(ctx.m());
+#ifdef USE_RPFP_CLONE
+	clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one
+      clone_rpfp = new RPFP_caching(clone_ls);
+      clone_rpfp->Clone(rpfp);
+#endif      
+#ifdef USE_NEW_GEN_CANDS
+      gen_cands_ls = new RPFP::iZ3LogicSolver(ctx);
+      gen_cands_rpfp = new RPFP_caching(gen_cands_ls);
+      gen_cands_rpfp->Clone(rpfp);
+#endif      
+      }
    }

+    ~Duality(){
+#ifdef USE_RPFP_CLONE
+      delete clone_rpfp;
+      delete clone_ls;
+#endif      
+#ifdef USE_NEW_GEN_CANDS
+      delete gen_cands_rpfp;
+      delete gen_cands_ls;
+#endif
+    }
+
+#ifdef USE_RPFP_CLONE
+    RPFP::LogicSolver *clone_ls;
+    RPFP_caching *clone_rpfp;
+#endif      
+#ifdef USE_NEW_GEN_CANDS
+    RPFP::LogicSolver *gen_cands_ls;
+    RPFP_caching *gen_cands_rpfp;
+#endif      
+
+
    typedef RPFP::Node Node;
    typedef RPFP::Edge Edge;

@ -804,8 +849,10 @@ namespace Duality {
 	Node *child = chs[i];
 	if(TopoSort[child] < TopoSort[node->map]){
 	  Node *leaf = LeafMap[child];
-	  if(!indset->Contains(leaf))
+	  if(!indset->Contains(leaf)){
+	    node->Outgoing->F.Formula = ctx.bool_val(false); // make this a proper leaf, else bogus cex
 	    return node->Outgoing;
+	  }
 	}
      }

@ -1085,7 +1132,8 @@ namespace Duality {
    void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){
      candidate.edge = edge;
      for(unsigned j = 0; j < edge->Children.size(); j++){
-	Edge *lb = root->Outgoing->Children[j]->Outgoing;
+	Node *node = root->Outgoing->Children[j];
+	Edge *lb = node->Outgoing;
 	std::vector<Node *> &insts = insts_of_node[edge->Children[j]];
 #ifndef MINIMIZE_CANDIDATES
 	for(int k = insts.size()-1; k >= 0; k--)
@ -1095,8 +1143,8 @@ namespace Duality {
 	{
 	  Node *inst = insts[k];
 	  if(indset->Contains(inst)){
-	    if(checker->Empty(lb->Parent) || 
-	       eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){
+	    if(checker->Empty(node) || 
+	       eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){
 	      candidate.Children.push_back(inst);
 	      goto next_child;
 	    }
@ -1166,6 +1214,25 @@ namespace Duality {
 #endif


+    Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){
+      Edge *gen_cands_edge = checker->GetEdgeClone(edge);
+      Node *root = gen_cands_edge->Parent;
+      root->Outgoing = gen_cands_edge;
+      GenNodeSolutionFromIndSet(edge->Parent, root->Bound);
+#if 0
+      if(root->Bound.IsFull())
+	return = 0;
+#endif
+      checker->AssertNode(root);
+      for(unsigned j = 0; j < edge->Children.size(); j++){
+	Node *oc = edge->Children[j];
+	Node *nc = gen_cands_edge->Children[j];
+        GenNodeSolutionWithMarkers(oc,nc->Annotation,true);
+      }
+      checker->AssertEdge(gen_cands_edge,1,true);
+      return root;
+    }
+
    /** If the current proposed solution is not inductive,
 	use the induction failure to generate candidates for extension. */
    void GenCandidatesFromInductionFailure(bool full_scan = false){
@ -1175,6 +1242,7 @@ namespace Duality {
 	Edge *edge = edges[i];
 	if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end())
 	  continue;
+#ifndef USE_NEW_GEN_CANDS
 	slvr.push();
 	RPFP *checker = new RPFP(rpfp->ls);
 	Node *root = CheckerForEdge(edge,checker);
@ -1186,6 +1254,18 @@ namespace Duality {
 	}
 	slvr.pop(1);
 	delete checker;
+#else
+	RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */);
+	gen_cands_rpfp->Push();
+	Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
+	if(gen_cands_rpfp->Check(root) != unsat){
+	  Candidate candidate;
+	  ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
+	  reporter->InductionFailure(edge,candidate.Children);
+	  candidates.push_back(candidate);
+	}
+	gen_cands_rpfp->Pop(1);
+#endif
      }
      updated_nodes.clear();
      timer_stop("GenCandIndFail");
@ -1309,6 +1389,9 @@ namespace Duality {
      node. */
    bool SatisfyUpperBound(Node *node){
      if(node->Bound.IsFull()) return true;
+#ifdef PROPAGATE_BEFORE_CHECK
+      Propagate();
+#endif
      reporter->Bound(node);
      int start_decs = rpfp->CumulativeDecisions();
      DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand);
@ -1412,13 +1495,77 @@ namespace Duality {
      }
    }

+    // Propagate conjuncts up the unwinding
+    void Propagate(){
+      reporter->Message("beginning propagation");
+      timer_start("Propagate");
+      std::vector<Node *> sorted_nodes = unwinding->nodes;
+      std::sort(sorted_nodes.begin(),sorted_nodes.end(),std::less<Node *>()); // sorts by sequence number
+      hash_map<Node *,std::set<expr> > facts;
+      for(unsigned i = 0; i < sorted_nodes.size(); i++){
+	Node *node = sorted_nodes[i];
+	std::set<expr> &node_facts = facts[node->map];
+	if(!(node->Outgoing && indset->Contains(node)))
+	  continue;
+	std::vector<expr> conj_vec;
+	unwinding->CollectConjuncts(node->Annotation.Formula,conj_vec);
+	std::set<expr> conjs;
+	std::copy(conj_vec.begin(),conj_vec.end(),std::inserter(conjs,conjs.begin()));
+	if(!node_facts.empty()){
+	  RPFP *checker = new RPFP(rpfp->ls);
+	  slvr.push();
+	  Node *root = checker->CloneNode(node);
+	  Edge *edge = node->Outgoing;
+	  // checker->AssertNode(root);
+	  std::vector<Node *> cs;
+	  for(unsigned j = 0; j < edge->Children.size(); j++){
+	    Node *oc = edge->Children[j];
+	    Node *nc = checker->CloneNode(oc);
+	    nc->Annotation = oc->Annotation; // is this needed?
+	    cs.push_back(nc);
+	  }
+	  Edge *checker_edge = checker->CreateEdge(root,edge->F,cs); 
+	  checker->AssertEdge(checker_edge, 0, true, false);
+	  std::vector<expr> propagated;
+	  for(std::set<expr> ::iterator it = node_facts.begin(), en = node_facts.end(); it != en;){
+	    const expr &fact = *it;
+	    if(conjs.find(fact) == conjs.end()){
+	      root->Bound.Formula = fact;
+	      slvr.push();
+	      checker->AssertNode(root);
+	      check_result res = checker->Check(root);
+	      slvr.pop();
+	      if(res != unsat){
+		std::set<expr> ::iterator victim = it;
+		++it;
+		node_facts.erase(victim); // if it ain't true, nix it
+		continue;
+	      }
+	      propagated.push_back(fact);
+	    }
+	    ++it;
+	  }
+	  slvr.pop();
+	  for(unsigned i = 0; i < propagated.size(); i++){
+	    root->Annotation.Formula = propagated[i];
+	    UpdateNodeToNode(node,root);
+	  }
+	  delete checker;
+	}
+	for(std::set<expr> ::iterator it = conjs.begin(), en = conjs.end(); it != en; ++it){
+	  expr foo = *it;
+	  node_facts.insert(foo);
+	}
+      }
+      timer_stop("Propagate");
+    }

    /** This class represents a derivation tree. */
    class DerivationTree {
    public:

      DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) 
-	: slvr(rpfp->slvr),
+	: slvr(rpfp->slvr()),
 	  ctx(rpfp->ctx)
      {
 	duality = _duality;
@ -1462,7 +1609,13 @@ namespace Duality {
 	constrained = _constrained;
 	false_approx = true;
 	timer_start("Derive");
+#ifndef USE_CACHING_RPFP
 	tree = _tree ? _tree : new RPFP(rpfp->ls);
+#else
+	RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx);
+	cache_ls->slvr->push();
+	tree = _tree ? _tree : new RPFP_caching(cache_ls);
+#endif
        tree->HornClauses = rpfp->HornClauses;
 	tree->Push(); // so we can clear out the solver later when finished
 	top = CreateApproximatedInstance(root);
@ -1474,19 +1627,28 @@ namespace Duality {
 	timer_start("Pop");
 	tree->Pop(1);
 	timer_stop("Pop");
+#ifdef USE_CACHING_RPFP
+	cache_ls->slvr->pop(1);
+	delete cache_ls;
+	tree->ls = rpfp->ls;
+#endif
 	timer_stop("Derive");
 	return res;
      }

 #define WITH_CHILDREN

-      Node *CreateApproximatedInstance(RPFP::Node *from){
-	Node *to = tree->CloneNode(from);
-	to->Annotation = from->Annotation;
+      void InitializeApproximatedInstance(RPFP::Node *to){
+	to->Annotation = to->map->Annotation;
 #ifndef WITH_CHILDREN
 	tree->CreateLowerBoundEdge(to);
 #endif
 	leaves.push_back(to);
+      }
+
+      Node *CreateApproximatedInstance(RPFP::Node *from){
+	Node *to = tree->CloneNode(from);
+	InitializeApproximatedInstance(to);
 	return to;
      }

@ -1555,13 +1717,23 @@ namespace Duality {

      virtual void ExpandNode(RPFP::Node *p){
 	// tree->RemoveEdge(p->Outgoing);
-	Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
-	std::vector<RPFP::Node *> &cs = edge->Children;
-	std::vector<RPFP::Node *> children(cs.size());
-	for(unsigned i = 0; i < cs.size(); i++)
-	  children[i] = CreateApproximatedInstance(cs[i]);
-	Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children);
-        ne->map = p->map->Outgoing->map;
+	Edge *ne = p->Outgoing;
+	if(ne) {
+	  // reporter->Message("Recycling edge...");
+	  std::vector<RPFP::Node *> &cs = ne->Children;
+	  for(unsigned i = 0; i < cs.size(); i++)
+	    InitializeApproximatedInstance(cs[i]);
+	  // ne->dual = expr();
+	}
+	else {
+	  Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
+	  std::vector<RPFP::Node *> &cs = edge->Children;
+	  std::vector<RPFP::Node *> children(cs.size());
+	  for(unsigned i = 0; i < cs.size(); i++)
+	    children[i] = CreateApproximatedInstance(cs[i]);
+	  ne = tree->CreateEdge(p, p->map->Outgoing->F, children);
+	  ne->map = p->map->Outgoing->map;
+	}
 #ifndef WITH_CHILDREN
 	tree->AssertEdge(ne);  // assert the edge in the solver
 #else
@ -1703,12 +1875,25 @@ namespace Duality {
      void RemoveExpansion(RPFP::Node *p){
 	Edge *edge = p->Outgoing;
 	Node *parent = edge->Parent; 
+#ifndef KEEP_EXPANSIONS
 	std::vector<RPFP::Node *> cs = edge->Children;
 	tree->DeleteEdge(edge);
 	for(unsigned i = 0; i < cs.size(); i++)
 	  tree->DeleteNode(cs[i]);
+#endif
 	leaves.push_back(parent);
      }
+      
+      // remove all the descendants of tree root (but not root itself)
+      void RemoveTree(RPFP *tree, RPFP::Node *root){
+	Edge *edge = root->Outgoing;
+	std::vector<RPFP::Node *> cs = edge->Children;
+	tree->DeleteEdge(edge);
+	for(unsigned i = 0; i < cs.size(); i++){
+	  RemoveTree(tree,cs[i]);
+	  tree->DeleteNode(cs[i]);
+	}
+      }
    };

    class DerivationTreeSlow : public DerivationTree {
@ -1730,13 +1915,14 @@ namespace Duality {

      virtual bool Build(){

-	stack.back().level = tree->slvr.get_scope_level();
+	stack.back().level = tree->slvr().get_scope_level();
+	bool was_sat = true;

 	while (true)
 	{
 	  lbool res;

-	  unsigned slvr_level = tree->slvr.get_scope_level();
+	  unsigned slvr_level = tree->slvr().get_scope_level();
 	  if(slvr_level != stack.back().level)
 	    throw "stacks out of sync!";

@ -1756,14 +1942,22 @@ namespace Duality {
 		tree->SolveSingleNode(top,node);
 		if(expansions.size() == 1 && NodeTooComplicated(node))
 		  SimplifyNode(node);
-		tree->Generalize(top,node);
+		else
+		  node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+		Generalize(node);
 		if(RecordUpdate(node))
 		  update_count++;
+		else
+		  heuristic->Update(node->map); // make it less likely to expand this node in future
 	      }
-	      if(update_count == 0)
+	      if(update_count == 0){
+		if(was_sat)
+		  throw Incompleteness();
 		reporter->Message("backtracked without learning");
+	      }
 	    }
 	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
+	    bool propagated = false;
 	    while(1) {
 	      std::vector<Node *> &expansions = stack.back().expansions;
 	      bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
@ -1787,28 +1981,42 @@ namespace Duality {
 		RemoveExpansion(node);
 	      }
 	      stack.pop_back();
-	      if(prev_level_used || stack.size() == 1) break;
+	      if(stack.size() == 1)break;
+	      if(prev_level_used){
+		Node *node = stack.back().expansions[0];
+		if(!Propagate(node)) break;
+		if(!RecordUpdate(node)) break; // shouldn't happen!
+		RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
+		propagated = true;
+		continue;
+	      }
+	      if(propagated) break;  // propagation invalidates the proof core, so disable non-chron backtrack
 	      RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
 	      std::vector<Node *> &unused_ex = stack.back().expansions;
 	      for(unsigned i = 0; i < unused_ex.size(); i++)
 		heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future
 	    } 
 	    HandleUpdatedNodes();
-	    if(stack.size() == 1)
+	    if(stack.size() == 1){
+	      if(top->Outgoing)
+		tree->DeleteEdge(top->Outgoing); // in case we kept the tree
 	      return false;
+	    }
+	    was_sat = false;
 	  }
 	  else {
+	    was_sat = true;
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
 #if 0
-	    if(tree->slvr.check() == unsat)
+	    if(tree->slvr().check() == unsat)
 	      throw "help!";
 #endif
 	    stack.push_back(stack_entry());
-	    stack.back().level = tree->slvr.get_scope_level();
+	    stack.back().level = tree->slvr().get_scope_level();
 	    if(ExpandSomeNodes(false,1)){
 	      continue;
 	    }
@ -1822,13 +2030,18 @@ namespace Duality {
      }
      
      bool NodeTooComplicated(Node *node){
+	int ops = tree->CountOperators(node->Annotation.Formula);
+	if(ops > 10) return true;
+	node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
 	return tree->CountOperators(node->Annotation.Formula) > 3;
      }

      void SimplifyNode(Node *node){
 	// have to destroy the old proof to get a new interpolant
+	timer_start("SimplifyNode");
 	tree->PopPush();
 	tree->InterpolateByCases(top,node);
+	timer_stop("SimplifyNode");
      }

      bool LevelUsedInProof(unsigned level){
@ -1927,6 +2140,39 @@ namespace Duality {
 	throw "can't unmap node";
      }

+      void Generalize(Node *node){
+#ifndef USE_RPFP_CLONE
+	tree->Generalize(top,node);
+#else
+	RPFP_caching *clone_rpfp = duality->clone_rpfp;
+	if(!node->Outgoing->map) return;
+	Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map);
+	Node *clone_node = clone_edge->Parent;
+	clone_node->Annotation = node->Annotation;
+	for(unsigned i = 0; i < clone_edge->Children.size(); i++)
+	  clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation;
+	clone_rpfp->GeneralizeCache(clone_edge);
+	node->Annotation = clone_node->Annotation;
+#endif
+      }
+
+      bool Propagate(Node *node){
+#ifdef USE_RPFP_CLONE
+	RPFP_caching *clone_rpfp = duality->clone_rpfp;
+	Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map);
+	Node *clone_node = clone_edge->Parent;
+	clone_node->Annotation = node->map->Annotation;
+	for(unsigned i = 0; i < clone_edge->Children.size(); i++)
+	  clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation;
+	bool res = clone_rpfp->PropagateCache(clone_edge);
+	if(res)
+	  node->Annotation = clone_node->Annotation;
+	return res;
+#else
+	return false;
+#endif
+      }
+
    };


@ -1948,6 +2194,11 @@ namespace Duality {
      Duality *parent;
      bool some_updates;

+#define NO_CONJ_ON_SIMPLE_LOOPS
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+      hash_set<Node *> simple_loops;
+#endif
+
      Node *&covered_by(Node *node){
 	return cm[node].covered_by;
      }
@ -1982,6 +2233,24 @@ namespace Duality {
      Covering(Duality *_parent){
 	parent = _parent;
 	some_updates = false;
+
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+	hash_map<Node *,std::vector<Edge *> > outgoing;
+	for(unsigned i = 0; i < parent->rpfp->edges.size(); i++)
+	  outgoing[parent->rpfp->edges[i]->Parent].push_back(parent->rpfp->edges[i]);
+	for(unsigned i = 0; i < parent->rpfp->nodes.size(); i++){
+	  Node * node = parent->rpfp->nodes[i];
+	  std::vector<Edge *> &outs = outgoing[node];
+	  if(outs.size() == 2){
+	    for(int j = 0; j < 2; j++){
+	      Edge *loop_edge = outs[j];
+	      if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent)
+		simple_loops.insert(node);
+	    }
+	  }
+	}
+#endif	
+
      }
      
      bool IsCoveredRec(hash_set<Node *> &memo, Node *node){
@ -2144,6 +2413,11 @@ namespace Duality {
      }

      bool CouldCover(Node *covered, Node *covering){
+#ifdef NO_CONJ_ON_SIMPLE_LOOPS
+	// Forsimple loops, we rely on propagation, not covering
+	if(simple_loops.find(covered->map) != simple_loops.end())
+	  return false;
+#endif
 #ifdef UNDERAPPROX_NODES
 	// if(parent->underapprox_map.find(covering) != parent->underapprox_map.end())
 	// return parent->underapprox_map[covering] == covered;
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@ -18,6 +18,13 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "duality_wrapper.h"
 #include <iostream>
 #include "smt_solver.h"
@ -30,10 +37,11 @@ Revision History:

 namespace Duality {

-  solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) {
+  solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) {
    params_ref p;
    p.set_bool("proof", true); // this is currently useless
-    p.set_bool("model", true); 
+    if(models)
+      p.set_bool("model", true); 
    p.set_bool("unsat_core", true); 
    p.set_bool("mbqi",true);
    p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
@ -44,6 +52,7 @@ namespace Duality {
    m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
    m_solver->updt_params(p); // why do we have to do this?
    canceled = false;
+    m_mode = m().proof_mode();
  }

 expr context::constant(const std::string &name, const sort &ty){ 
@ -338,6 +347,17 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
    return ctx().cook(result);
  }

+  expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
+    ::qe_lite qe(m());
+    expr_ref result(to_expr(raw()),m());
+    proof_ref pf(m());
+    uint_set uis;
+    for(std::set<int>::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it)
+      uis.insert(*it);
+    qe(uis,index_of_bound,result);
+    return ctx().cook(result);
+  }
+
  expr clone_quantifier(const expr &q, const expr &b){
    return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
  }
@ -362,6 +382,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
  }


+  unsigned func_decl::arity() const {
+    return (to_func_decl(raw())->get_arity());
+  }
+
+  sort func_decl::domain(unsigned i) const {
+    return sort(ctx(),(to_func_decl(raw())->get_domain(i)));
+  }
+
+  sort func_decl::range() const {
+    return sort(ctx(),(to_func_decl(raw())->get_range()));
+  }
+
  func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
    std::vector < ::sort * > _domain(domain.size());
    for(unsigned i = 0; i < domain.size(); i++)
@ -504,7 +536,10 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
 	  add(linear_assumptions[i][j]);
    }
    
-    check_result res = check();
+    check_result res = unsat;
+
+    if(!m_solver->get_proof())
+      res = check();
    
    if(res == unsat){

--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@ -26,6 +26,7 @@ Revision History:
 #include<sstream>
 #include<vector>
 #include<list>
+#include <set>
 #include"version.h"
 #include<limits.h>

@ -50,6 +51,7 @@ Revision History:
 #include"scoped_ctrl_c.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
+#include"scoped_proof.h"

 namespace Duality {

@ -449,6 +451,7 @@ namespace Duality {
        bool is_datatype() const { return get_sort().is_datatype(); }
        bool is_relation() const { return get_sort().is_relation(); }
        bool is_finite_domain() const { return get_sort().is_finite_domain(); }
+	bool is_true() const {return is_app() && decl().get_decl_kind() == True; }

        bool is_numeral() const {
 	  return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw()));
@ -560,6 +563,8 @@ namespace Duality {
 	
        expr qe_lite() const;

+	expr qe_lite(const std::set<int> &idxs, bool index_of_bound) const;
+
 	friend expr clone_quantifier(const expr &, const expr &);

        friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
@ -718,6 +723,7 @@ namespace Duality {
  	    m_model = s;
            return *this; 
        }
+	bool null() const {return !m_model;}
        
        expr eval(expr const & n, bool model_completion=true) const {
 	  ::model * _m = m_model.get();
@ -811,8 +817,9 @@ namespace Duality {
        ::solver *m_solver;
        model the_model;
 	bool canceled;
+	proof_gen_mode m_mode;
    public:
-        solver(context & c, bool extensional = false);
+        solver(context & c, bool extensional = false, bool models = true);
        solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
        solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;}
        ~solver() {
@ -824,6 +831,7 @@ namespace Duality {
            m_ctx = s.m_ctx; 
            m_solver = s.m_solver;
 	    the_model = s.the_model;
+	    m_mode = s.m_mode;
            return *this; 
        }
 	struct cancel_exception {};
@ -832,11 +840,12 @@ namespace Duality {
 	    throw(cancel_exception());
 	}
        // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
-        void push() { m_solver->push(); }
-        void pop(unsigned n = 1) { m_solver->pop(n); }
+        void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); }
+        void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); }
        // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); }
-        void add(expr const & e) { m_solver->assert_expr(e); }
+        void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); }
        check_result check() { 
+	  scoped_proof_mode spm(m(),m_mode); 
 	  checkpoint();
 	  lbool r = m_solver->check_sat(0,0);
 	  model_ref m;
@ -845,6 +854,7 @@ namespace Duality {
 	  return to_check_result(r);
 	}
        check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { 
+	  scoped_proof_mode spm(m(),m_mode); 
 	  model old_model(the_model);
 	  check_result res = check(n,assumptions,core_size,core);
 	  if(the_model == 0)
@ -852,6 +862,7 @@ namespace Duality {
 	  return res;
 	}
        check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) {
+	  scoped_proof_mode spm(m(),m_mode); 
 	  checkpoint();
 	  std::vector< ::expr *> _assumptions(n);
 	  for (unsigned i = 0; i < n; i++) {
@ -876,6 +887,7 @@ namespace Duality {
        }
 #if 0
        check_result check(expr_vector assumptions) { 
+	  scoped_proof_mode spm(m(),m_mode); 
            unsigned n = assumptions.size();
            z3array<Z3_ast> _assumptions(n);
            for (unsigned i = 0; i < n; i++) {
@ -900,17 +912,19 @@ namespace Duality {
 	int get_num_decisions(); 

 	void cancel(){
+	  scoped_proof_mode spm(m(),m_mode); 
 	  canceled = true;
 	  if(m_solver)
 	    m_solver->cancel();
 	}

-	unsigned get_scope_level(){return m_solver->get_scope_level();}
+	unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}

 	void show();
 	void show_assertion_ids();

 	proof get_proof(){
+	  scoped_proof_mode spm(m(),m_mode); 
 	  return proof(ctx(),m_solver->get_proof());
 	}

@ -1294,8 +1308,8 @@ namespace Duality {

    class interpolating_solver : public solver {
    public:
-    interpolating_solver(context &ctx)
-      : solver(ctx)
+    interpolating_solver(context &ctx, bool models = true)
+      : solver(ctx, true, models)
      {
 	weak_mode = false;
      }
@ -1359,6 +1373,21 @@ namespace Duality {
    typedef double clock_t;
    clock_t current_time();
    inline void output_time(std::ostream &os, clock_t time){os << time;}
+
+    template <class X> class uptr {
+    public:
+      X *ptr;
+      uptr(){ptr = 0;}
+      void set(X *_ptr){
+	if(ptr) delete ptr;
+	ptr = _ptr;
+      }
+      X *get(){ return ptr;}
+      ~uptr(){
+	if(ptr) delete ptr;
+      }
+    };
+
 };

 // to make Duality::ast hashable
@ -1393,6 +1422,18 @@ namespace std {
  };
 }

+// to make Duality::ast usable in ordered collections
+namespace std {
+  template <>
+    class less<Duality::expr> {
+  public:
+    bool operator()(const Duality::expr &s, const Duality::expr &t) const {
+      // return s.raw() < t.raw();
+      return s.raw()->get_id() < t.raw()->get_id();
+    }
+  };
+}
+
 // to make Duality::func_decl hashable
 namespace hash_space {
  template <>
@ -1425,6 +1466,5 @@ namespace std {
  };
 }

-
 #endif

--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@ -18,6 +18,12 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif

 #include "iz3base.h"
 #include <stdio.h>
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@ -17,6 +17,13 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3base.h"
 #include "iz3checker.h"

--- a/src/interp/iz3hash.h
+++ b/src/interp/iz3hash.h
@ -66,7 +66,7 @@ Revision History:
 namespace stl_ext {
  template <>
    class hash<std::string> {
-    stl_ext::hash<char *> H;
+    stl_ext::hash<const char *> H;
  public:
    size_t operator()(const std::string &s) const {
      return H(s.c_str());
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@ -18,6 +18,14 @@ Revision History:
 --*/

 /* Copyright 2011 Microsoft Research. */
+
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include <assert.h>
 #include <algorithm>
 #include <stdio.h>
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@ -18,6 +18,15 @@ Revision History:
 --*/


+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4805)
+#pragma warning(disable:4800)
+#endif
+
 #include "iz3mgr.h"

 #include <stdio.h>
@ -172,7 +181,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){


  std::vector<symbol> names;
-  std::vector<sort *> types;
+  std::vector<class sort *> types;
  std::vector<expr *>  bound_asts;
  unsigned num_bound = bvs.size();

@ -485,7 +494,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
  get_farkas_coeffs(proof,rats);
  coeffs.resize(rats.size());
  for(unsigned i = 0; i < rats.size(); i++){
-    sort *is = m().mk_sort(m_arith_fid, INT_SORT);
+    class sort *is = m().mk_sort(m_arith_fid, INT_SORT);
    ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
    coeffs[i] = coeff;
  }
@ -640,9 +649,9 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa

  /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */

-void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
+void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
  ast Qrhs;
-  bool strict = op(P) == Lt;
+  bool qstrict = false;
  if(is_not(Q)){
    ast nQ = arg(Q,0);
    switch(op(nQ)){
@ -654,11 +663,11 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
      break;
    case Geq:
      Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
-      strict = true;
+      qstrict = true;
      break;
    case Leq: 
      Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
-      strict = true;
+      qstrict = true;
      break;
    default:
      throw "not an inequality";
@ -674,28 +683,31 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q){
      break;
    case Lt:
      Qrhs = make(Sub,arg(Q,1),arg(Q,0));
-      strict = true;
+      qstrict = true;
      break;
    case Gt: 
      Qrhs = make(Sub,arg(Q,0),arg(Q,1));
-      strict = true;
+      qstrict = true;
      break;
    default:
      throw "not an inequality";
    }
  }
  Qrhs = make(Times,c,Qrhs);
+  bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+  if(pstrict && qstrict && round_off)
+    Qrhs = make(Sub,Qrhs,make_int(rational(1)));
  if(strict)
    P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
  else
    P = make(Leq,arg(P,0),make(Plus,arg(P,1),Qrhs));
 }

-iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs){
+iz3mgr::ast iz3mgr::sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off){
  ast zero = make_int("0");
  ast thing = make(Leq,zero,zero);
  for(unsigned i = 0; i < ineqs.size(); i++){
-    linear_comb(thing,coeffs[i],ineqs[i]);
+    linear_comb(thing,coeffs[i],ineqs[i], round_off);
  }
  thing = simplify_ineq(thing);
  return thing;
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@ -22,6 +22,7 @@ Revision History:


 #include <assert.h>
+#include <vector>
 #include "iz3hash.h"

 #include"well_sorted.h"
@ -262,6 +263,7 @@ class iz3mgr  {
    default:;    
    }
    assert(0);
+    return 0;
  }

  ast arg(const ast &t, int i){
@ -606,9 +608,9 @@ class iz3mgr  {
    return d;
  }
  
-  void linear_comb(ast &P, const ast &c, const ast &Q);
+  void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false);

-  ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs);
+  ast sum_inequalities(const std::vector<ast> &coeffs, const std::vector<ast> &ineqs, bool round_off = false);

  ast simplify_ineq(const ast &ineq){
    ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1)));
--- a/src/interp/iz3pp.cpp
+++ b/src/interp/iz3pp.cpp
@ -58,20 +58,20 @@ namespace stl_ext {
 class free_func_visitor {
  ast_manager& m;
  func_decl_set m_funcs;
-  obj_hashtable<sort> m_sorts;
+  obj_hashtable<class 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);
+    class 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; }
+  obj_hashtable<class sort>& sorts() { return m_sorts; }
 };

 class iz3pp_helper : public iz3mgr {
@ -146,8 +146,8 @@ void iz3pp(ast_manager &m,
  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();
+  obj_hashtable<class sort>& sorts = visitor.sorts();
+  obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();
  

  
--- a/src/interp/iz3profiling.cpp
+++ b/src/interp/iz3profiling.cpp
@ -17,6 +17,13 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3profiling.h"

 #include <map>
--- a/src/interp/iz3proof.cpp
+++ b/src/interp/iz3proof.cpp
@ -18,6 +18,12 @@ Revision History:
 --*/


+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif

 #include "iz3proof.h"
 #include "iz3profiling.h"
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@ -17,6 +17,13 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3proof_itp.h"

 #ifndef WIN32
@ -2170,7 +2177,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
    for(unsigned i = 0; i < prem_cons.size(); i++){
      const ast &lit = prem_cons[i];
      if(get_term_type(lit) == LitA)
-	linear_comb(thing,coeffs[i],lit);
+	// Farkas rule seems to assume strict integer inequalities are rounded
+	linear_comb(thing,coeffs[i],lit,true /*round_off*/);
    }
    thing = simplify_ineq(thing);
    for(unsigned i = 0; i < prem_cons.size(); i++){
@ -2195,9 +2203,9 @@ class iz3proof_itp_impl : public iz3proof_itp {

  /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */

-  void linear_comb(ast &P, const ast &c, const ast &Q){
+  void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false){
    ast Qrhs;
-    bool strict = op(P) == Lt;
+    bool qstrict = false;
    if(is_not(Q)){
      ast nQ = arg(Q,0);
      switch(op(nQ)){
@ -2209,11 +2217,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
      case Geq:
 	Qrhs = make(Sub,arg(nQ,1),arg(nQ,0));
-	strict = true;
+	qstrict = true;
 	break;
      case Leq: 
 	Qrhs = make(Sub,arg(nQ,0),arg(nQ,1));
-	strict = true;
+	qstrict = true;
 	break;
      default:
 	throw proof_error();
@ -2229,17 +2237,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
      case Lt:
 	Qrhs = make(Sub,arg(Q,1),arg(Q,0));
-	strict = true;
+	qstrict = true;
 	break;
      case Gt: 
 	Qrhs = make(Sub,arg(Q,0),arg(Q,1));
-	strict = true;
+	qstrict = true;
 	break;
      default:
 	throw proof_error();
      }
    }
    Qrhs = make(Times,c,Qrhs);
+    bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+    if(pstrict && qstrict && round_off)
+      Qrhs = make(Sub,Qrhs,make_int(rational(1)));
    if(strict)
      P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
    else
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@ -17,6 +17,13 @@ Revision History:

 --*/

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3translate.h"
 #include "iz3proof.h"
 #include "iz3profiling.h"
@ -1079,7 +1086,7 @@ public:
      my_cons.push_back(mk_not(arg(con,i)));
      my_coeffs.push_back(farkas_coeffs[i]);
    }
-    ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons));
+    ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */));
    my_cons.push_back(mk_not(farkas_con));
    my_coeffs.push_back(make_int("1"));
    std::vector<Iproof::node> my_hyps;
@ -1103,7 +1110,7 @@ public:
      my_cons.push_back(conc(prem(proof,i-1)));
      my_coeffs.push_back(farkas_coeffs[i]);
    }
-    ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons));
+    ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */));
    std::vector<Iproof::node> my_hyps;
    for(int i = 1; i < nargs; i++)
      my_hyps.push_back(prems[i-1]);
@ -1642,6 +1649,10 @@ public:
 	res = iproof->make_axiom(lits);
 	break;
      }
+      case PR_IFF_TRUE: { // turns p into p <-> true, noop for us
+	res = args[0];
+	break;
+      }
      default:
 	assert(0 && "translate_main: unsupported proof rule");
 	throw unsupported();
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@ -20,6 +20,14 @@ Revision History:
 --*/


+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4390)
+#endif
+
 #include "iz3translate.h"
 #include "iz3proof.h"
 #include "iz3profiling.h"
@ -58,7 +66,9 @@ namespace stl_ext {


 static int lemma_count = 0;
+#if 0
 static int nll_lemma_count = 0;
+#endif
 #define SHOW_LEMMA_COUNT -1

 // One half of a resolution. We need this to distinguish
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@ -35,10 +35,15 @@ Revision History:
 #include "model_smt2_pp.h"
 #include "model_v2_pp.h"
 #include "fixedpoint_params.hpp"
-#include "scoped_proof.h"

 // template class symbol_table<family_id>;

+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif

 #include "duality.h"
 #include "duality_profiling.h"
@ -213,6 +218,9 @@ lbool dl_interface::query(::expr * query) {
  catch (Duality::solver::cancel_exception &exn){
    throw default_exception("duality canceled");
  }
+  catch (Duality::Solver::Incompleteness &exn){
+    throw default_exception("incompleteness");
+  }
  
  // profile!

--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@ -759,7 +759,8 @@ namespace smt {
        app * fact     = to_app(m_manager.get_fact(pr));
        app * n1_owner = n1->get_owner();
        app * n2_owner = n2->get_owner();
-        if (fact->get_num_args() != 2 || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) {
+        bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact);
+        if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) {
            CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2),
                   tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n";
                   if (fact->get_num_args() == 2) {
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@ -1836,6 +1836,21 @@ 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 == 1 && m_bv_util.is_bv(args[0])) {
+        sort * s = f->get_range();
+        unsigned to_sbits = m_util.get_sbits(s);
+        unsigned to_ebits = m_util.get_ebits(s);
+
+        expr * bv = args[0];
+        int sz = m_bv_util.get_bv_size(bv);
+        SASSERT((unsigned)sz == to_sbits + to_ebits);
+
+        m_bv_util.mk_extract(sz - 1, sz - 1, bv);
+        mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
+                  m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
+                  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]))) {        
        // We also support float to float conversion
        sort * s = f->get_range();
@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
 }

+void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 3);
+    mk_triple(args[0], args[2], args[1], result);
+}
+
+void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
 void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
    SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
    SASSERT(to_app(e)->get_num_args() == 3);
--- a/src/tactic/fpa/fpa2bv_converter.h
+++ b/src/tactic/fpa/fpa2bv_converter.h
@ -122,7 +122,13 @@ public:
    void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

    void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);    
+    void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+
+    void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

    obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
    obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
--- a/src/tactic/fpa/fpa2bv_rewriter.h
+++ b/src/tactic/fpa/fpa2bv_rewriter.h
@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
            case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
            case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
            case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
            default:
                TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
--- a/src/tactic/fpa/qffpa_tactic.cpp
+++ b/src/tactic/fpa/qffpa_tactic.cpp
@ -36,3 +36,77 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
                    mk_sat_tactic(m, p),
                    mk_fail_if_undecided_tactic());
 }
+
+struct is_non_qffpa_predicate {
+    struct found {};
+    ast_manager & m;
+    float_util    u;
+
+    is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        sort * s = get_sort(n);
+        if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s)))
+            throw found();
+        family_id fid = s->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == u.get_family_id())
+            return;
+
+        throw found();
+    }
+};
+
+struct is_non_qffpabv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       bu;
+    float_util    fu;
+
+    is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        sort * s = get_sort(n);
+        if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s)))
+            throw found();
+        family_id fid = s->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == fu.get_family_id() || fid == bu.get_family_id())
+            return;
+
+        throw found();
+    }
+};
+
+class is_qffpa_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qffpa_predicate>(g);
+    }
+};
+
+class is_qffpabv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qffpabv_predicate>(g);
+    }
+};
+
+probe * mk_is_qffpa_probe() {
+    return alloc(is_qffpa_probe);
+}
+
+probe * mk_is_qffpabv_probe() {
+    return alloc(is_qffpabv_probe);
+}
+    
--- a/src/tactic/fpa/qffpa_tactic.h
+++ b/src/tactic/fpa/qffpa_tactic.h
@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref());
  ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)")
 */

+probe * mk_is_qffpa_probe();
+probe * mk_is_qffpabv_probe();
+/*
+  ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()")
+  ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()")
+*/
+
 #endif
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@ -27,6 +27,7 @@ Notes:
 #include"nra_tactic.h"
 #include"probe_arith.h"
 #include"quant_tactics.h"
+#include"qffpa_tactic.h"

 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
    tactic * st = using_params(and_then(mk_simplify_tactic(m),
@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                        cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
                                        cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                        cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
-                                             mk_smt_tactic())))))))),
+                                        cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p),
+                                             mk_smt_tactic()))))))))),
                               p);
    return st;
 }
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@ -49,8 +49,11 @@ Revision History:
 // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
 // the x87 FPU, even when /arch:SSE2 is on. 
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
+#ifdef __clang__
+#undef USE_INTRINSICS
+#else
 #include <emmintrin.h>
-
+#endif

 hwf_manager::hwf_manager() :
    m_mpz_manager(m_mpq_manager)
--- a/src/util/mpf.cpp
+++ b/src/util/mpf.cpp
@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
    return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
 }

+mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
+    return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
+}
+
 void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) {
    o.sbits = sbits;
    o.ebits = ebits;
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@ -182,6 +182,8 @@ public:
    mpf_exp_t mk_max_exp(unsigned ebits);
    mpf_exp_t mk_min_exp(unsigned ebits);

+    mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
+
    /**
       \brief Return the biggest k s.t. 2^k <= a.