diff --git a/src/duality/duality.h b/src/duality/duality.h
index 158ad84d9..fb3761626 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -142,6 +142,7 @@ namespace Duality {
            context *ctx;   /** Z3 context for formulas */
            solver *slvr;   /** Z3 solver */
            bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */
+	   solver aux_solver; /** For temporary use -- don't leave assertions here. */
 
            /** Tree interpolation. This method assumes the formulas in TermTree
                "assumptions" are currently asserted in the solver. The return
@@ -178,6 +179,8 @@ namespace Duality {
 	   /** Cancel, throw Canceled object if possible. */
 	   virtual void cancel(){ }
 
+           LogicSolver(context &c) : aux_solver(c){}
+
 	   virtual ~LogicSolver(){}
       };
 
@@ -215,7 +218,7 @@ namespace Duality {
         }
 #endif
 
-        iZ3LogicSolver(context &c){
+      iZ3LogicSolver(context &c) : LogicSolver(c) {
           ctx = ictx = &c;
           slvr = islvr = new interpolating_solver(*ictx);
           need_goals = false;
@@ -287,9 +290,9 @@ namespace Duality {
       literals dualLabels;
       std::list<stack_entry> stack;
       std::vector<Term> axioms; // only saved here for printing purposes
-      solver aux_solver;
-
-
+      solver &aux_solver;
+      hash_set<ast> *proof_core;
+      
     public:
 
       /** Construct an RPFP graph with a given interpolating prover context. It is allowed to
@@ -299,13 +302,14 @@ namespace Duality {
 	  inherit the axioms. 
       */
 
-    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)),	aux_solver(*(_ls->ctx))
+    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
       {
         ls = _ls;
 	nodeCount = 0;
 	edgeCount = 0;
 	stack.push_back(stack_entry());
         HornClauses = false;
+	proof_core = 0;
       }
 
       ~RPFP();
@@ -606,9 +610,13 @@ namespace Duality {
 
       lbool Solve(Node *root, int persist);
       
+      /** Same as Solve, but annotates only a single node. */
+
+      lbool SolveSingleNode(Node *root, Node *node);
+
       /** Get the constraint tree (but don't solve it) */
       
-      TermTree *GetConstraintTree(Node *root);
+      TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0);
   
       /** Dispose of the dual model (counterexample) if there is one. */
       
@@ -678,6 +686,12 @@ namespace Duality {
       /** Pop a scope (see Push). Note, you cannot pop axioms. */
       
       void Pop(int num_scopes);
+      
+      /** Return true if the given edge is used in the proof of unsat.
+	  Can be called only after Solve or Check returns an unsat result. */
+      
+      bool EdgeUsedInProof(Edge *edge);
+
 
       /** Convert a collection of clauses to Nodes and Edges in the RPFP.
 	  
@@ -762,8 +776,19 @@ namespace Duality {
 
       //      int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
 
+      /** Compute and save the proof core for future calls to
+	  EdgeUsedInProof.  You only need to call this if you will pop
+	  the solver before calling EdgeUsedInProof.
+       */
+      void ComputeProofCore();
+
     private:
       
+      void ClearProofCore(){
+	if(proof_core)
+	  delete proof_core;
+	proof_core = 0;
+      }
 
       Term SuffixVariable(const Term &t, int n);
       
@@ -779,10 +804,14 @@ namespace Duality {
 
       Term ReducedDualEdge(Edge *e);
 
-      TermTree *ToTermTree(Node *root);
+      TermTree *ToTermTree(Node *root, Node *skip_descendant = 0);
 
       TermTree *ToGoalTree(Node *root);
 
+      void CollapseTermTreeRec(TermTree *root, TermTree *node);
+
+      TermTree *CollapseTermTree(TermTree *node);
+
       void DecodeTree(Node *root, TermTree *interp, int persist);
 
       Term GetUpperBound(Node *n);
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 17e3de6bb..6b32bb080 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -185,6 +185,7 @@ namespace Duality {
     return clone_quantifier(t,new_body);
   }
 
+
   RPFP::Term RPFP::LocalizeRec(Edge *e,  hash_map<ast,Term> &memo, const Term &t)
   {
     std::pair<ast,Term> foo(t,expr(ctx));
@@ -274,13 +275,15 @@ namespace Duality {
     return implies(b, Localize(e, e->F.Formula));
   }
 
-  TermTree *RPFP::ToTermTree(Node *root)
+  TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant)
   {
+    if(skip_descendant && root == skip_descendant)
+      return new TermTree(ctx.bool_val(true));
     Edge *e = root->Outgoing;
     if(!e) return new TermTree(ctx.bool_val(true), std::vector<TermTree *>());
     std::vector<TermTree *> children(e->Children.size());
     for(unsigned i = 0; i < children.size(); i++)
-      children[i] = ToTermTree(e->Children[i]);
+      children[i] = ToTermTree(e->Children[i],skip_descendant);
     // Term top = ReducedDualEdge(e);
     Term top = e->dual.null() ? ctx.bool_val(true) : e->dual;
     TermTree *res = new TermTree(top, children);
@@ -623,6 +626,7 @@ namespace Duality {
     TermTree *goals = NULL;
     if(ls->need_goals)
       goals = GetGoalTree(root);
+    ClearProofCore();
 
     // if (dualModel != null) dualModel.Dispose();
     // if (dualLabels != null) dualLabels.Dispose();
@@ -644,11 +648,54 @@ namespace Duality {
     return res;
   }
   
+  void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){
+    root->addTerm(node->getTerm());
+    std::vector<Term> &cnsts = node->getTerms();
+    for(unsigned i = 0; i < cnsts.size(); i++)
+      root->addTerm(cnsts[i]);
+    std::vector<TermTree *> &chs = node->getChildren();
+    for(unsigned i = 0; i < chs.size(); i++){
+      CollapseTermTreeRec(root,chs[i]);
+    }
+  }
+
+  TermTree *RPFP::CollapseTermTree(TermTree *node){
+    std::vector<TermTree *> &chs = node->getChildren();
+    for(unsigned i = 0; i < chs.size(); i++)
+      CollapseTermTreeRec(node,chs[i]);
+    for(unsigned i = 0; i < chs.size(); i++)
+      delete chs[i];
+    chs.clear();
+    return node;
+  }
+    
+  lbool RPFP::SolveSingleNode(Node *root, Node *node)
+  {
+    timer_start("Solve");
+    TermTree *tree = CollapseTermTree(GetConstraintTree(root,node));
+    tree->getChildren().push_back(CollapseTermTree(ToTermTree(node)));
+    TermTree *interpolant = NULL;
+    ClearProofCore();
+
+    timer_start("interpolate_tree");
+    lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true);
+    timer_stop("interpolate_tree");
+    if (res == l_false)
+      {
+	DecodeTree(node, interpolant->getChildren()[0], 0);
+	delete interpolant;
+      }
+
+    delete tree;
+    timer_stop("Solve");
+    return res;
+  }
+
   /** Get the constraint tree (but don't solve it) */
   
-  TermTree *RPFP::GetConstraintTree(Node *root)
+  TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant)
   {
-    return AddUpperBound(root, ToTermTree(root));
+    return AddUpperBound(root, ToTermTree(root,skip_descendant));
   }
   
   /** Dispose of the dual model (counterexample) if there is one. */
@@ -677,6 +724,7 @@ namespace Duality {
 
   check_result RPFP::Check(Node *root, std::vector<Node *> underapproxes, std::vector<Node *> *underapprox_core )
         {
+	  ClearProofCore();
 	  // if (dualModel != null) dualModel.Dispose();
 	  check_result res;
 	  if(!underapproxes.size())
@@ -713,6 +761,7 @@ namespace Duality {
 
   check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
     // check_result temp1 = slvr.check(); // no idea why I need to do this
+    ClearProofCore();
     check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]);
     dualModel = slvr.get_model();
     return res;
@@ -1760,9 +1809,9 @@ namespace Duality {
     expr conj = ctx.make(And,conjuncts);
     s.add(conj);
     check_result res = s.check();
-    s.pop(1);
     if(res != unsat)
       throw "should be unsat";
+    s.pop(1);
 	
     for(unsigned i = 0; i < conjuncts.size(); ){
       std::swap(conjuncts[i],conjuncts.back());
@@ -2276,8 +2325,28 @@ namespace Duality {
     
   }
 
+  void RPFP::ComputeProofCore(){
+    if(!proof_core){
+      std::vector<expr> assumps;
+      slvr.get_proof().get_assumptions(assumps);
+      proof_core = new hash_set<ast>;
+      for(unsigned i = 0; i < assumps.size(); i++)
+	proof_core->insert(assumps[i]);
+    }
+  }
+
+  bool RPFP::EdgeUsedInProof(Edge *edge){
+    ComputeProofCore();
+    if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end())
+      return true;
+    for(unsigned i = 0; i < edge->constraints.size(); i++)
+      if(proof_core->find(edge->constraints[i]) != proof_core->end())
+	return true;
+    return false;
+  }
 
 RPFP::~RPFP(){
+    ClearProofCore();
     for(unsigned i = 0; i < nodes.size(); i++)
       delete nodes[i];
     for(unsigned i = 0; i < edges.size(); i++)
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index afa1c7683..86b95a657 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -184,7 +184,7 @@ namespace Duality {
 	    best.insert(*it);
       }
 #else
-      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false){
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false, bool best_only=false){
 	if(high_priority) return;
 	int best_score = INT_MAX;
 	int worst_score = 0;
@@ -194,13 +194,13 @@ namespace Duality {
 	  best_score = std::min(best_score,score);
 	  worst_score = std::max(worst_score,score);
 	}
-	int cutoff = best_score + (worst_score-best_score)/2;
+	int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2);
 	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it)
 	  if(scores[(*it)->map].updates <= cutoff)
 	    best.insert(*it);
       }
 #endif
-
+      
       /** Called when done expanding a tree */
       virtual void Done() {}
     };
@@ -1607,12 +1607,12 @@ namespace Duality {
 	heuristic->ChooseExpand(choices, best);
       }
 #else
-      void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority){
+      void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority, bool best_only = false){
 	std::set<Node *> choices;
 	for(std::list<RPFP::Node *>::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it)
 	  if (high_priority || !tree->Empty(*it)) // if used in the counter-model
 	    choices.insert(*it);
-	heuristic->ChooseExpand(choices, best, high_priority);
+	heuristic->ChooseExpand(choices, best, high_priority, best_only);
       }
 
       void ExpansionChoicesRec(std::vector <Node *> &unused_set, std::vector <Node *> &used_set, 
@@ -1650,9 +1650,9 @@ namespace Duality {
       
       std::set<Node *> old_choices;
 
-      void ExpansionChoices(std::set<Node *> &best, bool high_priority){
+      void ExpansionChoices(std::set<Node *> &best, bool high_priority, bool best_only = false){
 	if(!underapprox || constrained || high_priority){
-	  ExpansionChoicesFull(best, high_priority);
+	  ExpansionChoicesFull(best, high_priority,best_only);
 	  return;
 	}
 	std::vector <Node *> unused_set, used_set;
@@ -1684,7 +1684,7 @@ namespace Duality {
 	timer_start("ExpandSomeNodes");
 	timer_start("ExpansionChoices");
 	std::set<Node *> choices;
-	ExpansionChoices(choices,high_priority);
+	ExpansionChoices(choices,high_priority,max != INT_MAX);
 	timer_stop("ExpansionChoices");
 	std::list<RPFP::Node *> leaves_copy = leaves; // copy so can modify orig
 	leaves.clear();
@@ -1740,38 +1740,54 @@ namespace Duality {
 	  if(slvr_level != stack.back().level)
 	    throw "stacks out of sync!";
 
-	  res = tree->Solve(top, 1);            // incremental solve, keep interpolants for one pop
+	  //	  res = tree->Solve(top, 1);            // incremental solve, keep interpolants for one pop
+	  check_result foo = tree->Check(top);
+	  res = foo == unsat ? l_false : l_true;
 
 	  if (res == l_false) {
 	    if (stack.empty()) // should never happen
 	      return false;
 	    
-	    std::vector<Node *> &expansions = stack.back().expansions;
-	    int update_count = 0;
-	    for(unsigned i = 0; i < expansions.size(); i++){
-	      tree->Generalize(expansions[i]);
-	      if(RecordUpdate(expansions[i]))
-		update_count++;
-	    }
-	    if(update_count == 0)
-	      std::cout << "backtracked without learning\n";
-	    tree->Pop(1);	
-	    hash_set<Node *> leaves_to_remove;
-	    for(unsigned i = 0; i < expansions.size(); i++){
-	      Node *node = expansions[i];
-	      //	      if(node != top)
-	      //		tree->ConstrainParent(node->Incoming[0],node);
-	      std::vector<Node *> &cs = node->Outgoing->Children;
-	      for(unsigned i = 0; i < cs.size(); i++){
-		leaves_to_remove.insert(cs[i]);
-		UnmapNode(cs[i]);
-		if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
-		  throw "help!";
+	    {
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      int update_count = 0;
+	      for(unsigned i = 0; i < expansions.size(); i++){
+		Node *node = expansions[i];
+		tree->SolveSingleNode(top,node);
+		tree->Generalize(node);
+		if(RecordUpdate(node))
+		  update_count++;
 	      }
-	      RemoveExpansion(node);
+	      if(update_count == 0)
+		std::cout << "backtracked without learning\n";
 	    }
-	    RemoveLeaves(leaves_to_remove);
-	    stack.pop_back();
+	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
+	    while(1) {
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
+	      tree->Pop(1);	
+	      hash_set<Node *> leaves_to_remove;
+	      for(unsigned i = 0; i < expansions.size(); i++){
+		Node *node = expansions[i];
+		//	      if(node != top)
+		//		tree->ConstrainParent(node->Incoming[0],node);
+		std::vector<Node *> &cs = node->Outgoing->Children;
+		for(unsigned i = 0; i < cs.size(); i++){
+		  leaves_to_remove.insert(cs[i]);
+		  UnmapNode(cs[i]);
+		  if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
+		    throw "help!";
+		}
+		RemoveExpansion(node);
+	      }
+	      RemoveLeaves(leaves_to_remove);
+	      stack.pop_back();
+	      if(prev_level_used || stack.size() == 1) break;
+	      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)
 	      return false;
@@ -1782,8 +1798,10 @@ namespace Duality {
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
+#if 0
 	    if(tree->slvr.check() == unsat)
 	      throw "help!";
+#endif
 	    stack.push_back(stack_entry());
 	    stack.back().level = tree->slvr.get_scope_level();
 	    if(ExpandSomeNodes(false,1)){
@@ -1798,6 +1816,27 @@ namespace Duality {
 	}
       }
       
+      bool LevelUsedInProof(unsigned level){
+	std::vector<Node *> &expansions = stack[level].expansions;
+	for(unsigned i = 0; i < expansions.size(); i++)
+	  if(tree->EdgeUsedInProof(expansions[i]->Outgoing))
+	    return true;
+	return false;
+      }
+
+      void RemoveUpdateNodesAtCurrentLevel() {
+	for(std::list<Node *>::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){
+	  Node *node = *it;
+	  if(AtCurrentStackLevel(node->Incoming[0]->Parent)){
+	    std::list<Node *>::iterator victim = it;
+	    ++it;
+	    updated_nodes.erase(victim);
+	  }
+	  else
+	    ++it;
+	}
+      }
+
       void RemoveLeaves(hash_set<Node *> &leaves_to_remove){
 	std::list<RPFP::Node *> leaves_copy;
 	leaves_copy.swap(leaves);
@@ -2270,7 +2309,7 @@ namespace Duality {
 	return name;
       }
 
-      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority){
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
 	if(!high_priority || !old_cex.tree){
 	  Heuristic::ChooseExpand(choices,best,false);
 	  return;
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index dd64052a0..e70847d47 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -481,9 +481,9 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     for(unsigned i = 0; i < theory.size(); i++)
       _theory[i] = theory[i];
     
-    push();
     
     if(!incremental){
+      push();
       for(unsigned i = 0; i < linear_assumptions.size(); i++)
 	for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
 	  add(linear_assumptions[i][j]);
@@ -522,7 +522,8 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     }
 #endif
     
-    pop();
+    if(!incremental)
+      pop();
 
     return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef);
 
@@ -554,6 +555,29 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return "";
   }
 
+  
+  static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
+    if(memo.find(pf) != memo.end())return;
+    memo.insert(pf);
+    pfrule dk = pf.rule();
+    if(dk == PR_ASSERTED){
+      expr con = pf.conc();
+      assumps.push_back(con);
+    }
+    else {
+      unsigned nprems = pf.num_prems();
+      for(unsigned i = 0; i < nprems; i++){
+	proof arg = pf.prem(i);
+	get_assumptions_rec(memo,arg,assumps);
+      }
+    }
+  }
+
+  void proof::get_assumptions(std::vector<expr> &assumps){
+    stl_ext::hash_set<ast> memo;
+    get_assumptions_rec(memo,*this,assumps);
+  }
+
 
   void ast::show() const{
     std::cout << mk_pp(raw(), m()) << std::endl;
@@ -564,6 +588,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     std::cout << std::endl;
   }
   
+  void solver::show() {
+    unsigned n = m_solver->get_num_assertions();
+    if(!n)
+      return;
+    ast_smt_pp pp(m());
+    for (unsigned i = 0; i < n-1; ++i)
+      pp.add_assumption(m_solver->get_assertion(i));
+    pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
+  }
 
   void include_ast_show(ast &a){
     a.show();
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 291ddfbcf..fc94e53f2 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -393,6 +393,7 @@ namespace Duality {
       sort array_range() const;
     };
 
+    
     class func_decl : public ast {
     public:
         func_decl() : ast() {}
@@ -593,6 +594,36 @@ namespace Duality {
     };
     
 
+    typedef ::decl_kind pfrule;
+    
+    class proof : public ast {
+    public:
+      proof(context & c):ast(c) {}
+      proof(context & c, ::proof *s):ast(c, s) {}
+      proof(proof const & s):ast(s) {}
+      operator ::proof*() const { return to_app(raw()); }
+      proof & operator=(proof const & s) { return static_cast<proof&>(ast::operator=(s)); }
+
+      pfrule rule() const {
+	::func_decl *d = to_app(raw())->get_decl();
+	return d->get_decl_kind();
+      }
+
+      unsigned num_prems() const {
+	return to_app(raw())->get_num_args() - 1;
+      }
+      
+      expr conc() const {
+	return ctx().cook(to_app(raw())->get_arg(num_prems()));
+      }
+      
+      proof prem(unsigned i) const {
+	return proof(ctx(),to_app(to_app(raw())->get_arg(i)));
+      }
+      
+      void get_assumptions(std::vector<expr> &assumps);
+    };
+
 #if 0
 
 #if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3
@@ -870,6 +901,12 @@ namespace Duality {
 
 	unsigned get_scope_level(){return m_solver->get_scope_level();}
 
+	void show();
+
+	proof get_proof(){
+	  return proof(ctx(),m_solver->get_proof());
+	}
+
     };
 
 #if 0
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 7ef7e6aa2..9196e24d9 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -501,5 +501,3 @@ void interpolation_options_struct::apply(iz3base &b){
     b.set_option((*it).first,(*it).second);
 }
 
-
-
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 760feb000..6d0daa89a 100644
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -359,6 +359,12 @@ class iz3mgr  {
     return fid == m().get_basic_family_id() && k == BOOL_SORT;
   }
 
+  bool is_array_type(type t){
+    family_id fid = to_sort(t)->get_family_id(); 
+    decl_kind k = to_sort(t)->get_decl_kind();
+    return fid == m_array_fid && k == ARRAY_SORT;
+  }
+
   type get_range_type(symb s){
     return to_func_decl(s)->get_range();
   }
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 60bdcde9a..f8537d6eb 100644
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -473,7 +473,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
   hash_map<ast,ast> simplify_memo;
 
   ast simplify(const ast &t){
-    return simplify_rec(t);
+    ast res = normalize(simplify_rec(t));
+#ifdef BOGUS_QUANTS
+    if(localization_vars.size())
+      res = add_quants(z3_simplify(res));
+#endif
+    return res;
   }
 
   ast simplify_rec(const ast &e){
@@ -550,11 +555,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
   ast simplify_sum(std::vector<ast> &args){
-    ast cond = mk_true();
+    ast Aproves = mk_true(), Bproves = mk_true();
     ast ineq = args[0];
     if(!is_normal_ineq(ineq)) throw cannot_simplify();
-    sum_cond_ineq(ineq,cond,args[1],args[2]);
-    return my_implies(cond,ineq);
+    sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
+    return my_and(Aproves,my_implies(Bproves,ineq));
   }
 
   ast simplify_rotate_sum(const ast &pl, const ast &pf){
@@ -567,38 +572,42 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return sym(chain) == concat;
   }
   
-  ast ineq_from_chain(const ast &chain, ast &cond){
-    if(sym(chain) == normal)
-      throw "normalized inequalities not supported here";
-    if(is_rewrite_chain(chain)){
-      ast last = chain_last(chain);
-      ast rest = chain_rest(chain);
-      if(is_true(rest) && is_rewrite_side(LitA,last)
-	 && is_true(rewrite_lhs(last))){
-	cond = my_and(cond,rewrite_cond(last));
-	return rewrite_rhs(last);
-      }
-      if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last)))
-	return ineq_from_chain(rest,cond);
+#if 0
+  ast ineq_from_chain_simple(const ast &chain, ast &cond){
+    if(is_true(chain))
+      return chain;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    if(is_true(rest) && is_rewrite_side(LitA,last)
+       && is_true(rewrite_lhs(last))){
+      cond = my_and(cond,rewrite_cond(last));
+      return rewrite_rhs(last);
     }
+    if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last)))
+      return ineq_from_chain_simple(rest,cond);
+    return chain;
+  }
+#endif
+
+  ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){
+    if(is_rewrite_chain(chain))
+      return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
     return chain;
   }
 
-  void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){
+
+  void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
     opr o = op(ineq2);
     if(o == Implies){
-      sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1));
-      cond = my_and(cond,arg(ineq2,0));
+      sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
+      Bproves = my_and(Bproves,arg(ineq2,0));
     }
     else {
-      if(sym(ineq) == normal || sym(ineq2) == normal){
-	ast Aproves = mk_true();
-	sum_normal_ineq(ineq,coeff2,ineq2,Aproves,cond);
-	if(!is_true(Aproves))
-	  throw "Aproves not handled in sum_cond_ineq";
+      ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves);
+      if(sym(ineq) == normal || sym(the_ineq) == normal){
+	sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves);
 	return;
       }
-      ast the_ineq = ineq_from_chain(ineq2,cond);
       if(is_ineq(the_ineq))
 	linear_comb(ineq,coeff2,the_ineq);
       else 
@@ -621,10 +630,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast in1,in2,n1,n2;
     destruct_normal(ineq,in1,n1);
     destruct_normal(ineq2,in2,n2);
-    ast dummy;
-    sum_cond_ineq(in1,dummy,coeff2,in2);
+    ast dummy1, dummy2;
+    sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2);
     n1 = merge_normal_chains(n1,n2, Aproves, Bproves);
-    ineq = make(normal,in1,n1);
+    ineq = make_normal(in1,n1);
   }
 
   bool is_ineq(const ast &ineq){
@@ -639,7 +648,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast in1,n1;
       destruct_normal(ineq1,in1,n1);
       in1 = idiv_ineq(in1,divisor);
-      return make(normal,in1,n1);
+      return make_normal(in1,n1);
     }
     if(divisor == make_int(rational(1)))
       return ineq1;
@@ -649,17 +658,23 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
   }
   
-  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){
+  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
     if(pf == pl)
-      return my_implies(cond,simplify_ineq(ineq));
+      return my_implies(Bproves,simplify_ineq(ineq));
     if(op(pf) == Uninterpreted && sym(pf) == sum){
       if(arg(pf,2) == pl){
-	sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0));
+	ast Aproves = mk_true();
+	sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
+	if(!is_true(Aproves))
+	  throw "help!";
 	ineq = idiv_ineq(ineq,arg(pf,1));
-	return my_implies(cond,ineq);
+	return my_implies(Bproves,ineq);
       }
-      sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2));
-      return rotate_sum_rec(pl,arg(pf,0),cond,ineq);
+      ast Aproves = mk_true();
+      sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
+      if(!is_true(Aproves))
+	throw "help!";
+      return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
     }
     throw cannot_simplify();
   }
@@ -669,28 +684,30 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast equality = arg(neg_equality,0);
       ast x = arg(equality,0);
       ast y = arg(equality,1);
-      ast cond1 = mk_true();
-      ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1));
-      ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1));
+      ast Aproves1 = mk_true(), Bproves1 = mk_true();
+      ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1));
+      ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1));
       ast ineq1 = make(Leq,make_int("0"),make_int("0"));
-      sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy);
-      sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx);
-      cond1 = my_and(cond1,z3_simplify(ineq1));
-      ast cond2 = mk_true();
+      sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1);
+      sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1);
+      Bproves1 = my_and(Bproves1,z3_simplify(ineq1));
+      ast Aproves2 = mk_true(), Bproves2 = mk_true();
       ast ineq2 = make(Leq,make_int("0"),make_int("0"));
-      sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy);
-      sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx);
-      cond2 = z3_simplify(ineq2);
+      sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2);
+      sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
+      Bproves2 = z3_simplify(ineq2);
+      if(!is_true(Aproves1) || !is_true(Aproves2))
+	throw "help!";
       if(get_term_type(x) == LitA){
 	ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
-	ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter));
-	ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y));
+	ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter));
+	ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y));
 	return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
       }
       if(get_term_type(y) == LitA){
 	ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx)));
-	ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y));
-	ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter));
+	ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y));
+	ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter));
 	return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
       }
       throw cannot_simplify();
@@ -723,7 +740,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	}
 	else {
 	  ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
-	  return make(normal,itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
+	  return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
 	}
       }
     }
@@ -852,7 +869,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast sub_chain = extract_rewrites(chain,pos);
       if(is_true(sub_chain))
 	throw "bad inequality rewriting";
-      ast new_normal = make_normal(ineq2,ineq1,reverse_chain(sub_chain));
+      ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain));
       normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
     } 
   }
@@ -876,7 +893,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast mc = z3_simplify(chain_side_proves(LitA,pref));
       Aproves = my_and(Aproves,mc);
     }
-    return make(normal,itp,nc);
+    return make_normal(itp,nc);
   }
 
   /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */
@@ -913,7 +930,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast interp;
     if(is_normal_ineq(Q2)){ // inequalities are special
       ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
-      sum_cond_ineq(nQ2,Bproves,make_int(rational(1)),Q2);
+      sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves);
       interp = normalize(nQ2);
     }
     else 
@@ -1549,7 +1566,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	return;
       }
     }
-    if(op(ineq) == Leq){
+    if(op(ineq) == Leq || op(ineq) == Geq){
       lhs = srhs;
       rhs = arg(ineq,1);
       return;
@@ -1604,7 +1621,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
   ast normal_lhs(const ast &t){
-    return arg(arg(t,0),1);
+    return arg(arg(t,0),0);
   }
 
   ast normal_rhs(const ast &t){
@@ -1615,16 +1632,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return arg(t,1);
   }
 
-  ast make_normal(const ast &lhs, const ast &rhs, const ast &proof){
+  ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){
     return make(normal_step,make_equiv(lhs,rhs),proof);
   }
 
+  ast make_normal(const ast &ineq, const ast &nrml){
+    if(!is_ineq(ineq))
+      throw "what?";
+    return make(normal,ineq,nrml);
+  }
+
   ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
     LitType rhst = get_term_type(rhs);
     if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
-      return make_normal(lhs,rhs,proof);
+      return make_normal_step(lhs,rhs,proof);
     else
-      return make_normal(rhs,lhs,reverse_chain(proof));
+      return make_normal_step(rhs,lhs,reverse_chain(proof));
   }
 
   ast chain_side_proves(LitType side, const ast &chain){
@@ -1658,7 +1681,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){
       ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
       new_normal = f2;
-      trans[rhs1] = make_normal(rhs1,rhs2,new_proof);
+      trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof);
     }
     else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2))
       return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
@@ -1671,7 +1694,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       Aproves = my_and(Aproves,mcB);
       ast rep = apply_rewrite_chain(rhs1,Aproof);
       new_proof = concat_rewrite_chain(pf1,Aproof);
-      new_normal = make_normal(rhs1,rep,new_proof);
+      new_normal = make_normal_step(rhs1,rep,new_proof);
     }
     else if(t1 == LitA && t2 == LitB)
       return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
@@ -1701,7 +1724,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     if(it != trans.end()){
       const ast &f2 = it->second;
       ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
-      new_normal = make_normal(normal_lhs(f),normal_rhs(f2),pf);
+      new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
     }
     else
       new_normal = f;
@@ -1715,9 +1738,36 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return res;
   }
       
-  ast normalize(const ast &t){
+  bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){
+    if(op(t) == And){
+      Aproves = arg(t,0);
+      t = arg(t,1);
+    }
+    else
+      Aproves = mk_true();
+    if(op(t) == Implies){
+      Bproves = arg(t,0);
+      t = arg(t,1);
+    }
+    else
+      Bproves = mk_true();
+    if(is_normal_ineq(t)){
+      ineq = t;
+      return true;
+    }
+    return false;
+  }
+
+  ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){
+    return my_and(Aproves,my_implies(Bproves,ineq));
+  }
+
+  ast normalize(const ast &ct){
+    ast Aproves,Bproves,t;
+    if(!destruct_cond_ineq(ct,Aproves,Bproves,t))
+      return ct;
     if(sym(t) != normal)
-      return t;
+      return ct;
     ast chain = arg(t,1);
     hash_map<ast,ast> map;
     for(ast c = chain; !is_true(c); c = normal_rest(c)){
@@ -1727,7 +1777,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       map[lhs] = rhs;
     }
     ast res = subst(map,arg(t,0));
-    return res;
+    return cons_cond_ineq(Aproves,Bproves,res);
   }
   
   /** Make an assumption node. The given clause is assumed in the given frame. */
@@ -1848,8 +1898,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
   /** Make an axiom node. The conclusion must be an instance of an axiom. */
-  virtual node make_axiom(const std::vector<ast> &conclusion){
-    prover::range frng = pv->range_full();
+  virtual node make_axiom(const std::vector<ast> &conclusion, prover::range frng){
     int nargs = conclusion.size();
     std::vector<ast> largs(nargs);
     std::vector<ast> eqs;
@@ -1874,6 +1923,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return itp;
   }
 
+  virtual node make_axiom(const std::vector<ast> &conclusion){
+    return make_axiom(conclusion,pv->range_full());
+  }
+
   /** Make a Contra node. This rule takes a derivation of the form
      Gamma |- False and produces |- \/~Gamma. */
 
@@ -2299,7 +2352,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
       int nargs = num_args(e);
       if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
 	prover::range frng = rng;
-	if(op(e) == Uninterpreted){
+	opr o = op(e);
+	if(o == Uninterpreted){
 	  symb f = sym(e);
 	  prover::range srng = pv->sym_range(f);
 	  if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
@@ -2307,6 +2361,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	  else
 	    frng = srng; // this term will be localized
 	}
+	else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
+	  frng = erng; // this term will be localized
+	}
 	std::vector<ast> largs(nargs);
 	std::vector<ast> eqs;
 	std::vector<ast> pfs;
@@ -2333,6 +2390,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
     if(pv->ranges_intersect(pv->ast_scope(e),rng))
       return e; // this term occurs in range, so it's O.K.
 
+    if(is_array_type(get_type(e)))
+      throw "help!";
+
     // choose a frame for the constraint that is close to range
     int frame = pv->range_near(pv->ast_scope(e),rng);
 
@@ -2362,7 +2422,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
   /* Return an interpolant from a proof of false */
   ast interpolate(const node &pf){
     // proof of false must be a formula, with quantified symbols
+#ifndef BOGUS_QUANTS
     return add_quants(z3_simplify(pf));
+#else
+    return z3_simplify(pf);
+#endif
   }
 
   ast resolve_with_quantifier(const ast &pivot1, const ast &conj1,
diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h
index 299f391ea..4d76e3a92 100644
--- a/src/interp/iz3proof_itp.h
+++ b/src/interp/iz3proof_itp.h
@@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr {
   /** Make an axiom node. The conclusion must be an instance of an axiom. */
   virtual node make_axiom(const std::vector<ast> &conclusion) = 0;
 
+  /** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/
+  virtual node make_axiom(const std::vector<ast> &conclusion, prover::range) = 0;
+
   /** Make a Contra node. This rule takes a derivation of the form
      Gamma |- False and produces |- \/~Gamma. */
 
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 4ea755eff..7dfa48cdd 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1364,6 +1364,18 @@ public:
     return eq2;
   }
 
+  bool get_store_array(const ast &t, ast &res){
+    if(op(t) == Store){
+      res = t;
+      return true;
+    }
+    int nargs = num_args(t);
+    for(int i = 0; i < nargs; i++)
+      if(get_store_array(arg(t,i),res))
+	return true;
+    return false;
+  }
+
   // translate a Z3 proof term into interpolating proof system
 
   Iproof::node translate_main(ast proof, bool expect_clause = true){
@@ -1578,9 +1590,13 @@ public:
 	    throw unsupported();
 	  }
 	  break;
-	case ArrayTheory: // nothing fancy for this
-	  res = iproof->make_axiom(lits);
+	case ArrayTheory: {// nothing fancy for this
+	  ast store_array;
+	  if(!get_store_array(con,store_array))
+	    throw unsupported();
+	  res = iproof->make_axiom(lits,ast_scope(store_array));
 	  break;
+	}
 	default:
 	  throw unsupported();
 	}
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 25dfcebbd..12dd4ff3e 100644
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -472,7 +472,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
   expr conc = f(args);
   
 
-  ::vector<proof *> pprems;
+  ::vector< ::proof *> pprems;
   for(unsigned i = 0; i < prems.size(); i++)
     pprems.push_back(prems[i].get());