diff --git a/src/duality/duality.h b/src/duality/duality.h
index ef16696ec..343eeeb72 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -257,7 +257,9 @@ namespace Duality {
       };
       
       
+    public:
       model dualModel;
+    private:
       literals dualLabels;
       std::list<stack_entry> stack;
       std::vector<Term> axioms; // only saved here for printing purposes
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 77a007c82..623697880 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -248,6 +248,8 @@ namespace Duality {
   RPFP::Term RPFP::Localize(Edge *e, const Term &t){
     timer_start("Localize");
     hash_map<ast,Term> memo;
+    if(e->F.IndParams.size() > 0 && e->varMap.empty())
+      SetEdgeMaps(e); // TODO: why is this needed?
     Term res = LocalizeRec(e,memo,t);
     timer_stop("Localize");
     return res;
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 2fa46ba5a..9477ab0fa 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -688,10 +688,10 @@ namespace Duality {
         
         void show() const;
 
-        unsigned num_consts() const;
-        unsigned num_funcs() const;
-        func_decl get_const_decl(unsigned i) const;
-        func_decl get_func_decl(unsigned i) const;
+        unsigned num_consts() const {return m_model.get()->get_num_constants();}
+        unsigned num_funcs() const {return m_model.get()->get_num_functions();}
+        func_decl get_const_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_constant(i));}
+        func_decl get_func_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_function(i));}
         unsigned size() const;
         func_decl operator[](unsigned i) const;
 
diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp
index e49b89775..5922a8afd 100644
--- a/src/muz_qe/duality_dl_interface.cpp
+++ b/src/muz_qe/duality_dl_interface.cpp
@@ -35,6 +35,7 @@ Revision History:
 #include "dl_mk_coalesce.h"
 #include "expr_abstract.h"
 #include "model_smt2_pp.h"
+#include "model_v2_pp.h"
 
 // template class symbol_table<family_id>;
 
@@ -218,6 +219,8 @@ expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
 void dl_interface::reset_statistics() {
 }
 
+static hash_set<func_decl> *local_func_decls;
+
 static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) {
   context &ctx = d->dd()->ctx;
   RPFP::Node &node = *cex.root;
@@ -261,6 +264,8 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
       symbol name = t.get_quantifier_bound_name(j);
       expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
       out << "    (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n";
+      expr local_skolem = cex.tree->Localize(&edge,skolem);
+      (*local_func_decls).insert(local_skolem.decl());
     }
   }
   out << "  )\n";
@@ -298,8 +303,29 @@ void dl_interface::display_certificate(std::ostream& out) {
   else if(_d->status == StatusRefutation){
     out << "(derivation\n";
     // negation of the query is the last clause -- prove it
+    hash_set<func_decl> locals;
+    local_func_decls = &locals;
     print_proof(this,out,_d->cex);
     out << ")\n";
+    out << "(model \n";
+    ::model mod(m_ctx.get_manager());
+    model orig_model = _d->cex.tree->dualModel;
+    for(unsigned i = 0; i < orig_model.num_consts(); i++){
+      func_decl cnst = orig_model.get_const_decl(i);
+      if(locals.find(cnst) == locals.end()){
+	expr thing = orig_model.get_const_interp(cnst);
+	mod.register_decl(to_func_decl(cnst.raw()),to_expr(thing.raw()));
+      }
+    }
+    for(unsigned i = 0; i < orig_model.num_funcs(); i++){
+      func_decl cnst = orig_model.get_func_decl(i);
+      if(locals.find(cnst) == locals.end()){
+	func_interp thing = orig_model.get_func_interp(cnst);
+	mod.register_decl(to_func_decl(cnst.raw()),thing);
+      }
+    }
+    model_v2_pp(out,mod);
+    out << ")\n";
   }
 }