Index: /vis_dev/cusp-1.1/configure
===================================================================
--- /vis_dev/cusp-1.1/configure	(revision 39)
+++ /vis_dev/cusp-1.1/configure	(revision 40)
@@ -4815,7 +4815,7 @@
 # loading this file, other *unset* `ac_cv_foo' will be assigned the
 # following values.
-
-_ACEOF
-
+_ACEOF
+
+echo "lala"
 # The following way of writing the cache mishandles newlines in values,
 # but we know of no workaround that is simple, portable, and efficient.
Index: /vis_dev/cusp-1.1/helpers/mkinstalldirs
===================================================================
--- /vis_dev/cusp-1.1/helpers/mkinstalldirs	(revision 39)
+++ /vis_dev/cusp-1.1/helpers/mkinstalldirs	(revision 40)
@@ -6,5 +6,5 @@
 
 errstatus=0
-dirmode="."
+dirmode="./"
 
 usage="\
Index: /vis_dev/vis-2.3/models/debug/test.script
===================================================================
--- /vis_dev/vis-2.3/models/debug/test.script	(revision 39)
+++ /vis_dev/vis-2.3/models/debug/test.script	(revision 40)
@@ -1,5 +1,5 @@
 rlmv and2.mv
 init
-#_createAbn
+_createAbn
 aig
 _sat_debug  -k 1 -p and2.ltl -o and2_prop.cnf -v 1  
Index: /vis_dev/vis-2.3/models/transition/f.ctl
===================================================================
--- /vis_dev/vis-2.3/models/transition/f.ctl	(revision 39)
+++ /vis_dev/vis-2.3/models/transition/f.ctl	(revision 40)
@@ -1,1 +1,2 @@
 !EX(state[1:0] = 1);
+EX(state[1:0] = 3);
Index: /vis_dev/vis-2.3/models/transition/script
===================================================================
--- /vis_dev/vis-2.3/models/transition/script	(revision 39)
+++ /vis_dev/vis-2.3/models/transition/script	(revision 40)
@@ -2,3 +2,3 @@
 init
 compute_reach -v 1 
-_transition
+_transition -v 1
Index: /vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.c	(revision 39)
+++ /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 39)
+++ /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 39)
+++ /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;
+}
Index: /vis_dev/vis-2.3/src/ntk/ntkNtk.c
===================================================================
--- /vis_dev/vis-2.3/src/ntk/ntkNtk.c	(revision 39)
+++ /vis_dev/vis-2.3/src/ntk/ntkNtk.c	(revision 40)
@@ -1039,5 +1039,4 @@
     mAig_quit(network->mAigManager);
   }
-
   FREE(network);
 }