diff --git a/src/duality/duality.h b/src/duality/duality.h
index 16576dd65..edd89d78f 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -104,6 +104,8 @@ namespace Duality {
 
       FuncDecl RenumberPred(const FuncDecl &f, int n);
 
+      FuncDecl NumberPred(const FuncDecl &f, int n);
+
     Term ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming);
 
 
@@ -903,6 +905,10 @@ protected:
 
       int CumulativeDecisions();
 
+      void GreedyReduceNodes(std::vector<Node *> &nodes);
+
+      check_result CheckWithConstrainedNodes(std::vector<Node *> &posnodes,std::vector<Node *> &negnodes);
+
       solver &slvr(){
 	return *ls->slvr;
       }
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 8c88dda72..f2824c9b0 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -2816,6 +2816,62 @@ namespace Duality {
     }
   }
 
+  void foobar(){
+  }
+
+  void RPFP::GreedyReduceNodes(std::vector<Node *> &nodes){
+    std::vector<expr> lits;
+    for(unsigned i = 0; i < nodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(nodes[i], b, v);
+      lits.push_back(!b);
+      expr bv = dualModel.eval(b);
+      if(eq(bv,ctx.bool_val(true))){
+	check_result  res = slvr_check(lits.size(),&lits[0]);
+	if(res == unsat)
+	  lits.pop_back();
+	else
+	  foobar();
+      }
+    }
+  }
+
+  check_result RPFP::CheckWithConstrainedNodes(std::vector<Node *> &posnodes,std::vector<Node *> &negnodes){
+    timer_start("Check");
+    std::vector<expr> lits;
+    for(unsigned i = 0; i < posnodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(posnodes[i], b, v);
+      lits.push_back(b);
+    }
+    for(unsigned i = 0; i < negnodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(negnodes[i], b, v);
+      lits.push_back(!b);
+    }
+    check_result res = slvr_check(lits.size(),&lits[0]);
+    if(res == unsat && posnodes.size()){
+      lits.resize(posnodes.size());
+      res = slvr_check(lits.size(),&lits[0]);
+    }
+    dualModel = slvr().get_model();
+#if 0
+    if(!dualModel.null()){
+      std::cout << "posnodes called:\n";
+      for(unsigned i = 0; i < posnodes.size(); i++)
+	if(!Empty(posnodes[i]))
+	  std::cout << posnodes[i]->Name.name() << "\n";
+      std::cout << "negnodes called:\n";
+      for(unsigned i = 0; i < negnodes.size(); i++)
+	if(!Empty(negnodes[i]))
+	  std::cout << negnodes[i]->Name.name() << "\n";
+    }
+#endif
+    timer_stop("Check");
+    return res;
+  }
+
+
   void RPFP_caching::FilterCore(std::vector<expr> &core, std::vector<expr> &full_core){
     hash_set<ast> core_set;
     std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin()));
@@ -3333,6 +3389,17 @@ namespace Duality {
 	  return ctx.function(name.c_str(), arity, &domain[0], f.range());
         }
 
+  Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n)
+        {
+	  std::string name = f.name().str();
+	  name = name + "_" + string_of_int(n);
+	  int arity = f.arity();
+	  std::vector<sort> domain;
+	  for(int i = 0; i < arity; i++)
+	    domain.push_back(f.domain(i));
+	  return ctx.function(name.c_str(), arity, &domain[0], f.range());
+        }
+
   // Scan the clause body for occurrences of the predicate unknowns
 
   RPFP::Term RPFP::ScanBody(hash_map<ast,Term> &memo, 
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index f54e00693..49e591be2 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -255,6 +255,13 @@ namespace Duality {
       
       /** Called when done expanding a tree */
       virtual void Done() {}
+
+      /** Ask whether a node should be used/unused in the tree. Returns,
+	  1 if yes, -1 if no, and 0 if don't care. */
+
+      virtual int UseNode(Node *node){
+	return 0;
+      }
     };
     
     /** The Proposer class proposes conjectures eagerly. These can come
@@ -302,6 +309,7 @@ namespace Duality {
     hash_set<Node *> overapproxes;
     std::vector<Proposer *> proposers;
     std::string ConjectureFile;
+    bool stratified_inlining_done;
 
 #ifdef BOUNDED
     struct Counter {
@@ -314,6 +322,13 @@ namespace Duality {
     
     /** Solve the problem. */
     virtual bool Solve(){
+      PreSolve();
+      bool res = SolveMain();  // does the actual work
+      PostSolve();
+      return res;
+    }
+
+    void PreSolve(){
       reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
       conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile); 
 #ifndef LOCALIZE_CONJECTURES
@@ -342,9 +357,10 @@ namespace Duality {
 	  return false;
 #endif
       StratifiedLeafCount = -1;
-      timer_start("SolveMain");
-      bool res = SolveMain();  // does the actual work
-      timer_stop("SolveMain");
+      stratified_inlining_done = false;
+    }
+
+    void PostSolve(){
       //  print_profile(std::cout);
       delete indset;
       delete heuristic;
@@ -354,7 +370,16 @@ namespace Duality {
 	delete conj_reporter;
       for(unsigned i = 0; i < proposers.size(); i++)
 	delete proposers[i];
-      return res;
+    }
+
+    bool RecheckBounds(){
+      for(unsigned i = 0; i < unwinding->nodes.size(); i++){
+	Node *node = unwinding->nodes[i];
+	node->Bound = node->map->Bound;
+	if(!SatisfyUpperBound(node))
+	  return false;
+      }
+      return true;
     }
 
     void CreateInitialUnwinding(){
@@ -417,6 +442,7 @@ namespace Duality {
     bool StratifiedInlining; // Do stratified inlining as preprocessing step
     int RecursionBound;  // Recursion bound for bounded verification
     bool BatchExpand;
+    bool EnableRestarts; 
     
     bool SetBoolOption(bool &opt, const std::string &value){
       if(value == "0") {
@@ -464,6 +490,9 @@ namespace Duality {
       if(option == "conjecture_file"){
 	ConjectureFile = value;
       }
+      if(option == "enable_restarts"){
+        return SetBoolOption(EnableRestarts,value);
+      }
       return false;
     }
 
@@ -901,6 +930,9 @@ namespace Duality {
     */
 
     bool DoStratifiedInlining(){
+      if(stratified_inlining_done)
+	return true;
+      stratified_inlining_done = true;
       DoTopoSort();
       int depth = 1; // TODO: make this an option
       std::vector<hash_map<Node *,Node *> > unfolding_levels(depth+1);
@@ -1043,10 +1075,17 @@ namespace Duality {
 	h->SetOldNode(node);
     }
 
+    bool SolveMain(){
+      timer_start("SolveMain");
+      bool res = SolveMainInt();  // does the actual work
+      timer_stop("SolveMain");
+      return res;
+    }
+
     /** This does the actual solving work. We try to generate
 	candidates for extension. If we succed, we extend the
 	unwinding. If we fail, we have a solution. */
-    bool SolveMain(){
+    bool SolveMainInt(){
       if(StratifiedInlining && !DoStratifiedInlining())
 	return false;
 #ifdef BOUNDED
@@ -1776,6 +1815,7 @@ namespace Duality {
       }
       timer_stop("Propagate");
     }
+    
 
     /** This class represents a derivation tree. */
     class DerivationTree {
@@ -2127,6 +2167,8 @@ namespace Duality {
 
       hash_map<Node *, expr> updates;
 
+      int restart_interval;
+
       DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) 
 	: DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) {
 	stack.push_back(stack_entry());
@@ -2135,6 +2177,7 @@ namespace Duality {
       struct DoRestart {};
 
       virtual bool Build(){
+	restart_interval = 3;
 	while (true) {
 	  try {
 	    return BuildMain();
@@ -2145,15 +2188,47 @@ namespace Duality {
 	    while(stack.size() > 1)
 	      PopLevel();
 	    reporter->Message("restarted");
+	    restart_interval += 1;
 	  }
 	}
       }
 
+
+      // When we check, try to use the same children that were used in the
+      // previous counterexample.
+      check_result Check(){
+#if 0
+	std::vector<Node *> posnodes, negnodes;
+	std::vector<Node *> &expansions = stack.back().expansions;
+	for(unsigned i = 0; i < expansions.size(); i++){
+	  Node *node = expansions[i];
+	  std::vector<Node*> &chs = node->Outgoing->Children;
+	  for(unsigned j = 0; j < chs.size(); j++){
+	    Node *ch = chs[j];
+	    int use = heuristic->UseNode(ch); 
+	    if(use == 1)
+	      posnodes.push_back(ch);
+	    else if (use == -1)
+	      negnodes.push_back(ch);
+	  }
+	}
+	if(!(posnodes.empty() && negnodes.empty())){
+	  check_result res = tree->CheckWithConstrainedNodes(posnodes,negnodes);
+	  if(res != unsat){
+	    reporter->Message("matched previous counterexample");
+	    return res;
+	  }
+	}
+#endif
+	return tree->Check(top);
+      }
+
       bool BuildMain(){
 
 	stack.back().level = tree->slvr().get_scope_level();
 	bool was_sat = true;
 	int update_failures = 0;
+	int total_updates = 0;
 
 	while (true)
 	{
@@ -2165,7 +2240,7 @@ namespace Duality {
 	  reporter->Depth(stack.size());
 
 	  //	  res = tree->Solve(top, 1);            // incremental solve, keep interpolants for one pop
-	  check_result foo = tree->Check(top);
+	  check_result foo = Check();
 	  res = foo == unsat ? l_false : l_true;
 
 	  if (res == l_false) {
@@ -2193,11 +2268,18 @@ namespace Duality {
 		  throw DoRestart();
 		}
 #endif
-		if(RecordUpdate(node))
+		if(RecordUpdate(node)){
 		  update_count++;
+		  total_updates++;
+		}
 		else
 		  heuristic->Update(node->map); // make it less likely to expand this node in future
 	      }
+#if 1
+	      if(duality->EnableRestarts)
+		if(total_updates >= restart_interval)
+		  throw DoRestart();
+#endif
 	      if(update_count == 0){
 		if(was_sat){
 		  update_failures++;
@@ -2243,6 +2325,10 @@ namespace Duality {
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
 #ifndef NO_DECISIONS
+#if 0
+	    if(expansions.size() > 0)
+	      tree->GreedyReduceNodes(expansions[0]->Outgoing->Children); // try to reduce number of children
+#endif
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
@@ -2262,15 +2348,42 @@ namespace Duality {
 	    if(ExpandSomeNodes(false,expand_max))
 	      continue;
 	    tree->Pop(1);
+	    node_order.clear();
 	    while(stack.size() > 1){
 	      tree->Pop(1);	
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      for(unsigned i = 0; i < expansions.size(); i++)
+		node_order.push_back(expansions[i]);
 	      stack.pop_back();
 	    }
+#if 0
+	    Reduce();
+#endif
 	    return true;
 	  }
 	}
       }
       
+      std::vector<Node *> node_order;
+
+      void Reduce(){
+	tree->Push();
+	// tree->AssertNode(top); // assert the negation of the top-level spec
+	for(int i = node_order.size()-1; i >= 0; --i){
+	  Edge *edge = node_order[i]->Outgoing;
+	  if(edge){
+	    for(unsigned j = 0; j < edge->Children.size(); j++){
+	      Node *ch = edge->Children[j];
+	      if(!ch->Outgoing)
+		ch->Annotation.SetEmpty();
+	    }
+	    tree->AssertEdge(edge,0,true);
+	  }
+	}
+	tree->GreedyReduceNodes(node_order); // try to reduce the counterexample size
+	tree->Pop(1);
+      }
+
       void PopLevel(){
 	std::vector<Node *> &expansions = stack.back().expansions;
 	tree->Pop(1);	
@@ -2869,17 +2982,7 @@ namespace Duality {
 	return name;
       }
 
-      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.get_tree()){
-	  Heuristic::ChooseExpand(choices,best,false);
-	  return;
-	}
-	// first, try to match the derivatino tree nodes to the old cex
-	std::set<Node *> matched, unmatched;
-	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
-	  Node *node = (*it);
-	  if(cex_map.empty())
-	    cex_map[node] = old_cex.get_root();  // match the root nodes
+      Node *MatchNode(Node *node){
 	  if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node
 	    Node *parent = node->Incoming[0]->Parent; // assumes we are a tree!
 	    if(cex_map.find(parent) == cex_map.end())
@@ -2902,7 +3005,30 @@ namespace Duality {
 	      cex_map[chs[i]] = 0;
 	  }
 	matching_done:
-	  Node *old_node = cex_map[node];
+	  return cex_map[node];
+      }
+
+      int UseNode(Node *node){
+	if (!old_cex.get_tree())
+	  return 0;
+	Node *old_node = MatchNode(node);
+	if(!old_node)
+	  return 0;
+	return old_cex.get_tree()->Empty(old_node) ? -1 : 1;
+      }
+
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
+	if(cex_map.empty())
+	  cex_map[*(choices.begin())] = old_cex.get_root();  // match the root nodes
+	if(!high_priority || !old_cex.get_tree()){
+	  Heuristic::ChooseExpand(choices,best,false);
+	  return;
+	}
+	// first, try to match the derivatino tree nodes to the old cex
+	std::set<Node *> matched, unmatched;
+	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
+	  Node *node = (*it);
+	  Node *old_node = MatchNode(node);
 	  if(!old_node)
 	    unmatched.insert(node);
 	  else if(old_cex.get_tree()->Empty(old_node))
@@ -3177,8 +3303,233 @@ namespace Duality {
     
   };
 
+
+  class DualityDepthBounded : public Solver {
+
+    Duality *duality;
+    context &ctx;                        // Z3 context
+    solver &slvr;                        // Z3 solver
+
+  public:
+    DualityDepthBounded(RPFP *_rpfp) :
+      ctx(_rpfp->ctx),
+      slvr(_rpfp->slvr()){
+      rpfp = _rpfp;
+      DepthBoundRPFP();
+      duality = alloc(Duality,drpfp);
+    }
+
+    ~DualityDepthBounded(){
+      dealloc(duality);
+      delete drpfp;
+    }
+
+    bool Solve(){
+      int depth_bound = 10;
+      bool res;
+      SetMaxDepthRPFP(depth_bound);
+      duality->PreSolve();
+      while(true){
+	res = duality->SolveMain();
+	if(!res || GetSolution())
+	  break;
+	depth_bound++;
+	SetMaxDepthRPFP(depth_bound);
+	res = duality->RecheckBounds();
+	if(!res)
+	  break;
+      }
+      duality->PostSolve();
+      if(!res)
+	ConvertCex();
+      return res;
+    }
+
+    Counterexample &GetCounterexample(){
+      return cex;
+    }
+
+    bool SetOption(const std::string &option, const std::string &value){
+      return duality->SetOption(option,value);
+    }
+
+    virtual void LearnFrom(Solver *old_solver){
+      DualityDepthBounded *old = dynamic_cast<DualityDepthBounded *>(old_solver);
+      if(old){
+	duality->LearnFrom(old->duality);
+      }
+    }
+
+    bool IsResultRecursionBounded(){
+      return duality->IsResultRecursionBounded();
+    }
+
+    void Cancel(){
+      duality->Cancel();
+    }
+
+    typedef RPFP::Node Node;
+    typedef RPFP::Edge Edge;
+    RPFP *rpfp, *drpfp;
+    hash_map<Node *, Node *> db_map, db_rev_map;
+    hash_map<Edge *, Edge *> db_edge_rev_map;
+    std::vector<expr> db_saved_bounds;
+    Counterexample cex;
+
+    expr AddParamToRels(hash_map<ast,expr> &memo, hash_map<func_decl,func_decl> &rmap, const expr &p, const expr &t) {
+      std::pair<ast,expr> foo(t,expr(ctx));
+      std::pair<hash_map<ast,expr>::iterator, bool> bar = memo.insert(foo);
+      expr &res = bar.first->second;
+      if(!bar.second) return res;
+
+      if (t.is_app())
+	{
+	  func_decl f = t.decl();
+	  std::vector<expr> args;
+	  int nargs = t.num_args();
+	  for(int i = 0; i < nargs; i++)
+	    args.push_back(AddParamToRels(memo, rmap, p, t.arg(i)));
+	  hash_map<func_decl,func_decl>::iterator rit = rmap.find(f);
+	  if(rit != rmap.end()){
+	    args.push_back(p);
+	    res = (rit->second)(args);
+	    res = ctx.make(And,res,ctx.make(Geq,p,ctx.int_val(0)));
+	  }
+	  else
+	    res = f(args);
+	}
+      else if (t.is_quantifier())
+      {
+	expr body = AddParamToRels(memo, rmap, p, t.body());
+	res = clone_quantifier(t, body);
+      }
+      else res = t;
+      return res;
+    }
+
+
+    void DepthBoundRPFP(){
+      drpfp = new RPFP(rpfp->ls);
+      expr dvar = ctx.int_const("@depth");
+      expr dmax = ctx.int_const("@depth_max");
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++){
+	Node *node = rpfp->nodes[i];
+	std::vector<sort> arg_sorts;
+	const std::vector<expr> &params = node->Annotation.IndParams;
+	for(unsigned j = 0; j < params.size(); j++)
+	  arg_sorts.push_back(params[j].get_sort());
+	arg_sorts.push_back(ctx.int_sort());
+	std::string new_name = std::string("@db@") + node->Name.name().str();
+	func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort());
+	std::vector<expr> args = params;
+	args.push_back(dvar);
+	expr pat = f(args);
+	Node *dnode = drpfp->CreateNode(pat);
+	db_map[node] = dnode;
+	db_rev_map[dnode] = node;
+	expr bound_fmla = node->Bound.Formula;
+	if(!eq(bound_fmla,ctx.bool_val(true))){
+	  bound_fmla = implies(dvar == dmax,bound_fmla);
+	  dnode->Bound.Formula = bound_fmla;
+	}
+	db_saved_bounds.push_back(bound_fmla);
+	//	dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0)));
+      }
+      for(unsigned i = 0; i < rpfp->edges.size(); i++){
+	Edge *edge = rpfp->edges[i];
+	std::vector<Node *> new_children;
+	std::vector<func_decl> new_relparams;
+	hash_map<func_decl,func_decl> rmap;
+	for(unsigned j = 0; j < edge->Children.size(); j++){
+	  Node *ch = edge->Children[j];
+	  Node *nch = db_map[ch];
+	  func_decl f = nch->Name;
+	  func_decl sf = drpfp->NumberPred(f,j);
+	  new_children.push_back(nch);
+	  new_relparams.push_back(sf);
+	  rmap[edge->F.RelParams[j]] = sf;
+	}
+	std::vector<expr> new_indparams = edge->F.IndParams;
+	new_indparams.push_back(dvar);
+	hash_map<ast,expr> memo;
+	expr new_fmla = AddParamToRels(memo,rmap,ctx.make(Sub,dvar,ctx.int_val(1)),edge->F.Formula);
+	RPFP::Transformer new_t = drpfp->CreateTransformer(new_relparams,new_indparams,new_fmla);
+	Node *new_parent = db_map[edge->Parent];
+	db_edge_rev_map[drpfp->CreateEdge(new_parent,new_t,new_children)] = edge;
+      }
+    }
+
+    void SetMaxDepthRPFP(int depth){
+      hash_map<ast,expr> subst;
+      expr dmax = ctx.int_const("@depth_max");
+      subst[dmax] = ctx.int_val(depth);
+      for(unsigned i = 0; i < drpfp->nodes.size(); i++){
+	Node *node = drpfp->nodes[i];
+	expr fmla = db_saved_bounds[i];
+	fmla = drpfp->SubstRec(subst,fmla);
+	node->Bound.Formula = fmla;
+      }
+    }
+
+    void ConvertCex(){
+      cex.clear();
+      RPFP *tree = new RPFP(rpfp->ls);
+      Node *root;
+      Counterexample &dctx = duality->GetCounterexample();
+      hash_map<Node *, Node *> ctx_node_map;
+      for(unsigned i = 0; i < dctx.get_tree()->nodes.size(); i++){
+	Node *dnode = dctx.get_tree()->nodes[i];
+	Node *onode = db_rev_map[dnode->map->map];
+	Node *node = tree->CloneNode(onode);
+	node->number = dnode->number; // numbers have to match for model to make sense
+	ctx_node_map[dnode] = node;
+	if(dnode == dctx.get_root())
+	  root = node;
+      }
+      for(unsigned i = 0; i < dctx.get_tree()->edges.size(); i++){
+	Edge *dedge = dctx.get_tree()->edges[i];
+	Edge *oedge = db_edge_rev_map[dedge->map];
+	Node *parent = ctx_node_map[dedge->Parent];
+	std::vector<Node *> chs;
+	for(unsigned j = 0; j < dedge->Children.size(); j++)
+	  chs.push_back(ctx_node_map[dedge->Children[j]]);
+	Edge *edge = tree->CreateEdge(parent,oedge->F,chs);
+	edge->number = dedge->number; // numbers have to match for model to make sense
+	edge->map = oedge;
+      }
+      tree->dualModel = dctx.get_tree()->dualModel;
+      cex.set(tree,root);
+    }
+
+    bool GetSolution(){
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++)
+	if(!drpfp->nodes[i]->Annotation.SubsetEq(rpfp->nodes[i]->Bound))
+	  return false;
+      expr dvar = ctx.int_const("@depth");
+      hash_map<ast,expr> subst;
+      subst[dvar] = ctx.int_val(INT_MAX);
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++){
+	expr fmla = drpfp->nodes[i]->Annotation.Formula;
+	fmla = drpfp->SubstRec(subst,fmla);
+	fmla = fmla.simplify();
+	rpfp->nodes[i]->Annotation.Formula = fmla;
+      }
+      return true;
+    }
+
+    void UndoDepthBoundRPFP(){
+#if 0
+      if(cex.get_tree()){
+	// here, need to map the cex back...
+      }
+      // also need to map the proof back, but we don't...
+#endif
+    }
+  };
+
   Solver *Solver::Create(const std::string &solver_class, RPFP *rpfp){
-    Duality *s = alloc(Duality,rpfp);
+    //    Solver *s = alloc(DualityDepthBounded,rpfp);
+    Solver *s = alloc(Duality,rpfp);
     return s;
   }
 
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 5bfbba6b2..832e3329e 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -78,6 +78,7 @@ def_module_params('fixedpoint',
 			  ('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'),
+			  ('enable_restarts', BOOL, False, 'DUALITY: enable restarts'),
                           ))
 
 
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 08c57b05e..55f6c3747 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -281,6 +281,7 @@ lbool dl_interface::query(::expr * query) {
   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());
+  rs->SetOption("enable_restarts",m_ctx.get_params().enable_restarts() ? "1" : "0");
 #if 0
   if(rb != UINT_MAX){
     std::ostringstream os; os << rb;