diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 14fe545e0..0b1c688b9 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -513,6 +513,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
 	opts.set("weak","1"); 
       
       ::ast *proof = m_solver->get_proof();
+      show_assertion_ids();
       iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
       
       std::vector<expr> linearized_interpolants(_interpolants.size());
@@ -613,6 +614,14 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
   }
 
+  void solver::show_assertion_ids() {
+    unsigned n = m_solver->get_num_assertions();
+    std::cerr << "assertion ids: ";
+    for (unsigned i = 0; i < n-1; ++i)
+      std::cerr << " " << m_solver->get_assertion(i)->get_id();
+    std::cerr << "\n";
+  }
+
   void include_ast_show(ast &a){
     a.show();
   }
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index fec1f08d1..f0988013d 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -907,6 +907,7 @@ namespace Duality {
 	unsigned get_scope_level(){return m_solver->get_scope_level();}
 
 	void show();
+	void show_assertion_ids();
 
 	proof get_proof(){
 	  return proof(ctx(),m_solver->get_proof());