Index: vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.c	(revision 38)
+++ vis_dev/vis-2.3/src/debug/debug.c	(revision 40)
@@ -296,4 +296,5 @@
     return 1;
   }
+
   /*
     We need the bdd when building the transition relation of the automaton
@@ -308,5 +309,6 @@
     }
   }
-
+Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
+printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
 /*
  * Read the formula
@@ -394,52 +396,16 @@
     int l;
     // return the clause number
-    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
+    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    
     int leftValue   = checkIndex(noLoopIndex, cnfClauses);
     printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
-    int rightValue,loop,andIndex;
-    array_t           *orClause = NIL(array_t);
-    array_t           *loopClause, *tmpclause;
-
-    if (leftValue != 1) {
-      orClause = array_alloc(int, 0);   
-      if (leftValue == -1){
-	    array_insert_last(int, orClause, noLoopIndex);
-      }
-      loopClause = array_alloc(int, k+1);
-      for(l=0; l<=k; l++){
-	    int loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
-	    rightValue = checkIndex(loopIndex, cnfClauses);
-	  if (rightValue == 0){
-	    break;
-	  }
-      if (rightValue !=0){
-	    loop = cnfClauses->cnfGlobalIndex++;
-	    BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
-						nodeToMvfAigTable, CoiTable, loop);
-	  array_insert(int, loopClause, l, loop);
-	  if(rightValue == -1){
-	    
-	    andIndex   = cnfClauses->cnfGlobalIndex++;
-	    tmpclause  = array_alloc(int, 2);
-	    array_insert(int, tmpclause, 0, loop);
-	    array_insert(int, tmpclause, 1, -andIndex);
-	    BmcCnfInsertClause(cnfClauses, tmpclause);
-
-	    array_insert(int, tmpclause, 0, loopIndex);
-	    array_insert(int, tmpclause, 1, -andIndex);
-	    BmcCnfInsertClause(cnfClauses, tmpclause);
-        array_free(tmpclause);
-	    array_insert_last(int, orClause, andIndex);
-      }
-      else {
-	    array_insert_last(int, orClause, loop);
-	  }
-      }} // for l loop 
-      }
-       BmcCnfInsertClause(cnfClauses, orClause);
-        array_free(orClause);
-
-
+	array_t           *objClause = NIL(array_t);
+	objClause = array_alloc(int, 0);   
+	array_insert_last(int, objClause, noLoopIndex);
+	BmcCnfInsertClause(cnfClauses, objClause);
+    array_free(objClause);
+
+	
+//TODO Add abnormal formula 
 
 
Index: vis_dev/vis-2.3/src/debug/debug.h
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.h	(revision 38)
+++ vis_dev/vis-2.3/src/debug/debug.h	(revision 40)
@@ -55,5 +55,5 @@
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
-
+#define DBG_NETWORK_APPL_KEY "Dbg_NetworkApplKey"
 
 /*---------------------------------------------------------------------------*/
@@ -124,5 +124,6 @@
 EXTERN void Debug_End(void);
 EXTERN Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network);
-EXTERN void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
+EXTERN void Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn);
+EXTERN void Dbg_AbnormalFreeCallback(void *data);
 EXTERN void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal);
 EXTERN void Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode);
@@ -130,4 +131,5 @@
 EXTERN array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal);
 EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
+EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
 /**AutomaticEnd***************************************************************/
 
Index: vis_dev/vis-2.3/src/debug/debugAbnormal.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debugAbnormal.c	(revision 38)
+++ vis_dev/vis-2.3/src/debug/debugAbnormal.c	(revision 40)
@@ -114,4 +114,7 @@
 	}
 }
+ Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
+ (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
+ (void *) abnormal);
 }
 /**Function********************************************************************
@@ -157,4 +160,24 @@
 	 FREE(abn);
 }	
+/**Function********************************************************************
+
+  Synopsis    [Call-back function to free an abnormal structure.]
+
+  Description [This function will be stored in the network together with the
+  pointer to the structure. Whenever the network deletes the partitioning
+  information, this function is called and it will deallocate the abnormal and
+  the information attached to it.]
+
+  SideEffects []
+
+  SeeAlso     [Ntk_NetworkAddApplInfo]
+
+******************************************************************************/
+void
+Dbg_AbnormalFreeCallback(
+   void *data)
+{
+  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
+} /* End of Part_PartitionFreeCallback */
 
 
@@ -227,3 +250,19 @@
 	return abnormal->abnormal;
 }
-
+/**Function********************************************************************
+ 
+  Synopsis    [returns the abnormal structure]
+
+  Description [returns the abnormal structure associated to the network]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
+{
+	Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);
+
+	return abn;
+}