diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index e201c2a19..5bfbba6b2 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -77,6 +77,7 @@ def_module_params('fixedpoint',
 			  ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
 			  ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
                           ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
+			  ('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
                           ))
 
 
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 99ac2ee1c..e23f3f7ef 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -211,6 +211,7 @@ lbool dl_interface::query(::expr * query) {
   rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
   rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
   rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
+  rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
   unsigned rb = m_ctx.get_params().recursion_bound();
   if(rb != UINT_MAX){
     std::ostringstream os; os << rb;