diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index bbd1ebe0a..69759f9bb 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -802,6 +802,15 @@ namespace Duality {
       annot.Simplify();
     }    
 
+    bool NodeSolutionFromIndSetFull(Node *node){
+      std::vector<Node *> &insts = insts_of_node[node];
+      for(unsigned j = 0; j < insts.size(); j++)
+	if(indset->Contains(insts[j]))
+	  if(insts[j]->Annotation.IsFull())
+	    return true;
+      return false;
+    }
+
     bool recursionBounded;
 
     /** See if the solution might be bounded. */
@@ -1453,16 +1462,18 @@ namespace Duality {
 	slvr.pop(1);
 	delete checker;
 #else
-	RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
-	gen_cands_rpfp->Push();
-	Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
-	if(gen_cands_rpfp->Check(root) != unsat){
-	  Candidate candidate;
-	  ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
-	  reporter->InductionFailure(edge,candidate.Children);
-	  candidates.push_back(candidate);
+	if(!NodeSolutionFromIndSetFull(edge->Parent)){
+	  RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
+	  gen_cands_rpfp->Push();
+	  Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
+	  if(gen_cands_rpfp->Check(root) != unsat){
+	    Candidate candidate;
+	    ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
+	    reporter->InductionFailure(edge,candidate.Children);
+	    candidates.push_back(candidate);
+	  }
+	  gen_cands_rpfp->Pop(1);
 	}
-	gen_cands_rpfp->Pop(1);
 #endif
       }
       updated_nodes.clear();
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index c7fa0a08f..9a6d0c633 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -158,26 +158,7 @@ lbool dl_interface::query(::expr * query) {
   vector<unsigned> bounds;
   // m_ctx.get_rules_as_formulas(rules, names);
 
-  expr_ref query_ref(m_ctx.get_manager());
-  if(****){
-    m_ctx.flush_add_rules();
-    datalog::rule_manager& rm = m_ctx.get_rule_manager();
-    rm.mk_query(query, m_ctx.get_rules());
-    apply_default_transformation(m_ctx);
-    rule_set &rs = m_ctx.get_rules();
-    if(m_ctx.get_rules().get_output_predicates().empty())
-      query_ref = m_ctx.get_manager().mk_true();
-    else {
-          query_pred = m_ctx.get_rules().get_output_predicate();
-	  func_decl_ref query_pred(m_ctx.get_manager());
-	  query_pred = m_ctx.get_rules().get_output_predicate();
-	  ptr_vector<sort> sorts;
-	  unsi
-
-    }
-  }
-  else 
-    m_ctx.get_raw_rule_formulas(rules, names, bounds);
+  m_ctx.get_raw_rule_formulas(rules, names, bounds);
 
   // get all the rules as clauses
   std::vector<expr> &clauses = _d->clauses;