Index: vis_dev/vis-2.3/src/bmc/bmcInt.h
===================================================================
--- vis_dev/vis-2.3/src/bmc/bmcInt.h	(revision 40)
+++ vis_dev/vis-2.3/src/bmc/bmcInt.h	(revision 41)
@@ -184,5 +184,5 @@
 EXTERN Ltl_Automaton_t * BmcAutLtlToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula);
 EXTERN void BmcAutTerminationFree(BmcCheckForTermination_t *result);
-EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *options);
+EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *savons);
 EXTERN Bmc_PropertyStatus BmcBddSatCheckLtlFormula(Ntk_Network_t *network, mdd_t *initialStates, mdd_t *targetStates, BmcOption_t *options, st_table *CoiTable);
 EXTERN void BmcLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
Index: vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.c	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debug.c	(revision 41)
@@ -65,4 +65,5 @@
 static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 
 
@@ -94,4 +95,5 @@
   Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
   Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
+  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
 
 }
@@ -176,27 +178,4 @@
 
 ******************************************************************************/
-static int
-checkIndex(
-  int             index,
-  BmcCnfClauses_t *cnfClauses)
-{
-  int     rtnValue = -1; /* it is not TRUE or FALSE*/
-
-  if (index == 0){ /* TRUE or FALSE*/
-    if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
-      rtnValue = 0; /* FALSE */
-    } else {
-      /*
-	if (cnfClauses->noOfClauses == 0)
-	rtnValue = 1;
-	}
-      */
-      rtnValue = 1; /* TRUE */
-    }
-  }
-  return rtnValue;
-}
-
-
 static int 
 CommandSatDebug(
@@ -206,145 +185,71 @@
 int            c,i;
 int            verbose = 0;              /* default value */
-BmcOption_t  *options = BmcOptionAlloc();
-Ntk_Network_t * network;
-bAig_Manager_t    *manager;
-array_t           *formulaArray;
-array_t           *LTLformulaArray;
-char *ltlFileName     = NIL(char);
+BmcOption_t      * options = BmcOptionAlloc();
+Ntk_Network_t    * network;
+bAig_Manager_t   * manager;
+array_t          * formulaArray;
+array_t          * LTLformulaArray;
+char             * ltlFileName     = NIL(char);
+
 
 /*
  * Parse command line options.
  */
-util_getopt_reset();
-while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
-  switch(c) {
-    case 'v':
-      verbose = 1;
-	  options->verbosityLevel =  verbose;
-      break;
-    case 'h':
-      goto usage;
-	case 'm':
-      for (i = 0; i < strlen(util_optarg); i++) {
-		if (!isdigit((int)util_optarg[i])) {
-			goto usage;
-		}
-      }
-      options->minK = atoi(util_optarg);
-      break;
-    case 'k':
-      for (i = 0; i < strlen(util_optarg); i++) {
-		if (!isdigit((int)util_optarg[i])) {
-			goto usage;
-		}
-      }
-	  options->maxK = atoi(util_optarg);
-	  break;
-	case 'o':
-      options->cnfFileName = util_strsav(util_optarg);
-      break;
-    case 'p':
-      ltlFileName     = util_strsav(util_optarg);
-    break;
-
-    default:
-      goto usage;
-  }
-}
+if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
+     return 1;
+}
+
+
 printf("MAX K %d", options->maxK);
- if (options->minK > options->maxK){
-    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");    
-    goto usage;
-  }
 
 if (verbose) {
   (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
 }
- /* create SAT Solver input file */
- if (options->cnfFileName == NIL(char)) {
-    options->satInFile = BmcCreateTmpFile(); 
-}
- else {
-    options->satInFile = options->cnfFileName;
- }
-
-/* create SAT Solver output file */
-options->satOutFile = BmcCreateTmpFile();
-if (options->satOutFile == NIL(char)){
+/*
+ *  Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
   BmcOptionFree(options);
- (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
   return 1;
 }
-
-options->verbosityLevel =  1;
-//options->satSolver
-//options->clauses 
-
- /*
-   * Read the network
-   */
-  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
-  if (network == NIL(Ntk_Network_t)) {
-    (void) fprintf(vis_stdout, "** bmc error: No network\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-  manager = Ntk_NetworkReadMAigManager(network);
-  if (manager == NIL(mAig_Manager_t)) {
-    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-
-  /*
-    We need the bdd when building the transition relation of the automaton
-  */
-  if(options->inductiveStep !=0){
-    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
- 
-    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
-    if (designFsm == NIL(Fsm_Fsm_t)) {
-	 (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
-      return 1;
-    }
-  }
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
+  BmcOptionFree(options);
+  return 1;
+}
+
 Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
-printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
-/*
- * Read the formula
- */
- /* Read LTL Formulae */
-  if (!ltlFileName) 
-      goto usage;
-
-  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
-  if (options->ltlFile == NIL(FILE)) {
-    (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
-    FREE(ltlFileName);
-    BmcOptionFree(options);
-  }
-  FREE(ltlFileName);
-
- formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
-  if (formulaArray == NIL(array_t)) {
-    (void) fprintf(vis_stderr,
-		   "** bmc error: error in parsing CTL* Fromula from file\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-  if (array_n(formulaArray) == 0) {
-    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
-    BmcOptionFree(options);
-    Ctlsp_FormulaArrayFree(formulaArray);
-    return 1;
-  }
-  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+if(abn == NIL(Dbg_Abnormal_t)){
+  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
+  return 1;
+}
+if(verbose)
+  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
+
+
+formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
+if (formulaArray == NIL(array_t)) {
+  (void) fprintf(vis_stderr,
+  	   "** bmc error: error in parsing CTL* Fromula from file\n");
+  BmcOptionFree(options);
+  return 1;
+}
+if (array_n(formulaArray) == 0) {
+  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
+  BmcOptionFree(options);
   Ctlsp_FormulaArrayFree(formulaArray);
-  if (LTLformulaArray ==  NIL(array_t)){
-    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
-    BmcOptionFree(options);
-    return 1;
-  }
-    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
+  return 1;
+}
+LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
+Ctlsp_FormulaArrayFree(formulaArray);
+if (LTLformulaArray ==  NIL(array_t)){
+  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
+  BmcOptionFree(options);
+  return 1;
+}
+Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
 
 
@@ -353,4 +258,5 @@
     Compute the cone of influence 
 	here : a list of state variables (latches)
+    TODO refine to COI of the property
   */
 	st_table        *CoiTable =  generateAllLatches(network);
@@ -359,33 +265,12 @@
       clauses in BMC.
     */
-    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
-	BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
-    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
-	/*
-    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
-    */
-	nodeToMvfAigTable =
-	(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
-	assert(nodeToMvfAigTable != NIL(st_table));
-
-	if(verbose)
+  	if(verbose)
 	{	
-		(void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
-		printLatch(nodeToMvfAigTable);
 		(void) fprintf(vis_stdout, "------      COI       ----\n");
 		printLatch(CoiTable);
 		(void) fprintf(vis_stdout, "--------------------------\n");
     }
-    /*
-      Create a clause database
-     */
-    cnfClauses = BmcCnfClausesAlloc();
-    /*
-      Generate clauses for an initialized path of length k
-     */
-    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
-     fprintf(vis_stdout, "\n");
-    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
-				 cnfClauses, nodeToMvfAigTable, CoiTable);
+    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
+
 
     //Generate ltl CNF
@@ -393,4 +278,6 @@
     // aprÃšs il faut ajouter l'objectif de l'index avec boucle ou pas ...
     // cf. BmcLtlVerifyGeneralLtl
+    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
+    fprintf(vis_stdout, "\n");
     int k = options->maxK;
     int l;
@@ -398,6 +285,5 @@
     int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    
-    int leftValue   = checkIndex(noLoopIndex, cnfClauses);
-    printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue); 
+
 	array_t           *objClause = NIL(array_t);
 	objClause = array_alloc(int, 0);   
@@ -406,10 +292,33 @@
     array_free(objClause);
 
-	
-//TODO Add abnormal formula 
-
-
-
-
+	//Add Abnormal
+    st_table * nodeToMvfAigTable =  NIL(st_table);
+    nodeToMvfAigTable =
+(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+assert(nodeToMvfAigTable != NIL(st_table));
+
+    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
+
+      //loop abnormal
+    int aIndex;
+    Ntk_Node_t * abnNode;
+     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
+     if(aIndex<=0){
+     //set abnormal
+      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
+      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
+      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
+      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
+
+      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+      fclose(cnfFile);
+
+      //SAT procedure 
+      int res = Dbg_SatCheck("assig",options->cnfFileName);
+
+        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
+        }
+     }
 
 	 if(verbose)
@@ -417,22 +326,150 @@
 		latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    	
- Ctlsp_FormulaArrayFree(LTLformulaArray);    
-	BmcWriteClauses(manager, cnfFile, cnfClauses, options);
-fclose(cnfFile);
+Ctlsp_FormulaArrayFree(LTLformulaArray);    
 BmcCnfClausesFree(cnfClauses);
 BmcOptionFree(options);
 return 0;
-  usage:
-  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
-  minimum length] [-o cnf_file] [-p ltl_file]\n");
-  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
-  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
-  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n");  
+ 
+}
+/**Function********************************************************************
+
+  Synopsis    [Implements the generate_network_cnf.]
+
+  CommandName [generate_network_cnf]
+
+  CommandSynopsis [generate a CNF view of the network]
+
+  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
+  
+  CommandDescription [This command geerate a CNF of the network in DMACS form.
+  The network may be unroll within k steps.
+  <p>
+
+  Command options:<p>  
+
+  <dl>
+  <dt> -h
+  <dd> Print the command usage.
+  </dl>
+
+  <dt> -v
+  <dd> Verbose mode.
+  </dl>
+
+  <dt> -k
+  <dd> number of steps (default 1).
+  </dl>
+  ]
+
+  SideEffects []
+
+******************************************************************************/
+
+static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
+{
+  BmcOption_t  *options = BmcOptionAlloc();
+  int c;
+  unsigned int i;
+  Ntk_Network_t * network;
+  bAig_Manager_t   * manager;
+  char *  outName = NIL(char);
+   FILE *cnfFile;
+  if (!options){
+    return 1;
+  }
+  options->dbgOut = 0;
+  /*
+   * Parse command line options.
+   */
+  util_getopt_reset();
+  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
+    switch(c) {
+    case 'h':
+      goto usage;
+    case 'k':
+      options->maxK = atoi(util_optarg);
+      break;
+    case 'v':
+      for (i = 0; i < strlen(util_optarg); i++) {
+	if (!isdigit((int)util_optarg[i])) {
+	  goto usage;
+	}
+      }
+      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
+      break;
+    default:
+      goto usage;
+    }
+  }
+   if (argc - util_optind != 0)
+   {
+      outName  = util_strsav(argv[util_optind]);
+      /* create SAT Solver input file */
+     options->cnfFileName= outName;
+    options->satInFile = options->cnfFileName;
+    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
+  }
+  
+ 
+/*
+ *  Read the network
+ */
+network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if (network == NIL(Ntk_Network_t)) {
+  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
+  BmcOptionFree(options);
+  return 1;
+}
+manager = Ntk_NetworkReadMAigManager(network);
+if (manager == NIL(mAig_Manager_t)) {
+  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
+  BmcOptionFree(options);
+  return 1;
+}
+
+ /*
+    Compute the cone of influence 
+	here : a list of state variables (latches)
+  */
+st_table        *CoiTable =  generateAllLatches(network);
+
+if(options->verbosityLevel)
+{	
+	(void) fprintf(vis_stdout, "------      COI       ----\n");
+	printLatch(CoiTable);
+	(void) fprintf(vis_stdout, "--------------------------\n");
+}
+BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
+  if(outName != NIL(char))
+  {
+    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+    fclose(cnfFile);
+  }
+  else
+     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
+
+if(options->verbosityLevel)
+{	
+	(void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
+    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
+    st_count(CoiTable));
+} 
+    
+BmcOptionFree(options);
+ return 0;
+ usage:
+  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
+  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
   (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
-  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n");  
-  (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n");  
-  return 1;		/* error exit */
-
-}
+  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
+  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
+  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
+
+  BmcOptionFree(options);
+  return 1;
+}
+
 /**Function********************************************************************
 
Index: vis_dev/vis-2.3/src/debug/debug.h
===================================================================
--- vis_dev/vis-2.3/src/debug/debug.h	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debug.h	(revision 41)
@@ -132,4 +132,12 @@
 EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
 EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
+EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t   * manager,
+st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses);
+EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName);
+EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network, 
+BmcOption_t * option, st_table  *CoiTable);
+
+
+
 /**AutomaticEnd***************************************************************/
 
Index: vis_dev/vis-2.3/src/debug/debugAbnormal.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debugAbnormal.c	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debugAbnormal.c	(revision 41)
@@ -138,4 +138,6 @@
 	 abn->abnormal = array_alloc(Ntk_Node_t*,0);
 	 abn->freeInputs = array_alloc(Ntk_Node_t*,0);
+     abn->abnAigArray = NIL(array_t);
+     abn->abnCnfIndexArray = NIL(array_t);
 	 abn->verbose = 0;
 	 return abn;
@@ -158,4 +160,6 @@
 	 array_free(abn->abnormal);
 	 array_free(abn->freeInputs);
+     array_free(abn->abnCnfIndexArray);
+     array_free(abn->abnAigArray);
 	 FREE(abn);
 }	
@@ -267,2 +271,64 @@
 	return abn;
 }
+/**Function********************************************************************
+ 
+  Synopsis    [Initialize the abnormal predicate in the clauses array abni =0]
+
+  Description [Fill the Dbg data structure, abnAigArray conains the set of Aig 
+  for the set of abnormal perdicate. Each abnormal are set to zero in the clause
+  array.predicabnCnfIndexArray is the cnf index. The   correspondance is made by
+  the index in the table, the index of a node in   abnArray is the same in
+  abnAigArray and in abnIndexArray. If this array were  alredy computed nothing
+  is done, if the aig or index information either.]
+
+  SideEffects [Fill abnAigArray and abnCnfIndexArray]
+
+  SeeAlso     []
+
+******************************************************************************/
+void Dbg_InitAbn(Dbg_Abnormal_t * abn,
+bAig_Manager_t   * manager,
+st_table * nodeToMvfAigTable,
+BmcCnfClauses_t *cnfClauses)
+{
+  if(abn->abnAigArray != NIL(array_t))
+    (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
+  if(abn->abnCnfIndexArray != NIL(array_t)){
+    (void) fprintf(vis_stdout, "Abnormal index alredy filled\n"); 
+     return;
+  }
+  //Fill
+   int size = array_n(abn->abnormal);
+   array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
+   array_t * abnIndexArray = array_alloc(int,size);
+   int aIndex;
+   Ntk_Node_t * abnNode;
+   Dbg_ForEachAbnormal(abn, aIndex,abnNode){
+   MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
+    if (abnMvfAig ==  NIL(MvfAig_Function_t)){
+     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
+     create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
+     return ;
+    }
+    int mvfSize   = array_n(abnMvfAig);
+    int i;
+    bAigEdge_t         * abnBAig  = ALLOC(bAigEdge_t, mvfSize);
+
+    for(i=0; i< mvfSize; i++)
+    {
+      abnBAig[i] = bAig_GetCanonical(manager,
+      MvfAig_FunctionReadComponent(abnMvfAig,  i));
+    }
+    array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
+    int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
+    array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
+    // Create clause
+     array_t           *abnClause = NIL(array_t);
+	 abnClause = array_alloc(int, 0);   
+	 array_insert_last(int, abnClause, abnIndex);
+	 BmcCnfInsertClause(cnfClauses, abnClause);
+     array_free(abnClause);
+   }
+   abn->abnAigArray = abnAigArray;
+   abn->abnCnfIndexArray = abnIndexArray;
+}
Index: vis_dev/vis-2.3/src/debug/debugInt.h
===================================================================
--- vis_dev/vis-2.3/src/debug/debugInt.h	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debugInt.h	(revision 41)
@@ -55,4 +55,6 @@
 	array_t * abnormal; /* Array of Ntk_Node_t* */
 	array_t * freeInputs; /* Array of Ntk_Node_t* */
+	array_t * abnAigArray; /* Array of bAigEdge_t* as many entries as possible value */
+	array_t * abnCnfIndexArray; /* Array of int */
 	int verbose;
 };
Index: vis_dev/vis-2.3/src/debug/debugUtilities.c
===================================================================
--- vis_dev/vis-2.3/src/debug/debugUtilities.c	(revision 40)
+++ vis_dev/vis-2.3/src/debug/debugUtilities.c	(revision 41)
@@ -87,2 +87,107 @@
   return;
 }
+/**Function********************************************************************
+ 
+  Synopsis    [Performs the sat call]
+
+  Description [Retrun the result of SAT call, avec positionnement des options]
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+
+int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
+)
+{
+ satManager_t *cm;
+ cm = sat_InitManager(0);
+ cm->comment = ALLOC(char, 2);
+ cm->comment[0] = ' ';
+ cm->comment[1] = '\0';
+ cm->stdOut = stdout;
+ cm->stdErr = stderr;
+
+ 
+  satOption_t  *satOption;
+  array_t      *result = NIL(array_t);
+  int          maxSize;
+
+  satOption = sat_InitOption();
+  satOption->verbose = 2;
+  //satOption->unsatCoreFileName = "Ucore.txt";
+  satOption->clauseDeletionHeuristic = 0;
+  //satOption->coreGeneration = 1 ;
+  //satOption->minimizeConflictClause = 1;
+  if(forceAssigName != NULL)
+    satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
+   cm->option = satOption;
+   cm->each = sat_InitStatistics();
+
+  cm->unitLits = sat_ArrayAlloc(16);
+  cm->pureLits = sat_ArrayAlloc(16);
+
+  maxSize = 1024 << 8;
+  cm->nodesArray = ALLOC(long, maxSize);
+  cm->maxNodesArraySize = maxSize;
+  cm->nodesArraySize = satNodeSize;
+
+  sat_AllocLiteralsDB(cm);
+
+   sat_ReadCNF(cm,cnfFileName);
+   sat_Main(cm);
+
+   if(cm->status == SAT_UNSAT) {
+    if(cm->option->forcedAssignArr)
+      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
+	      cm->comment);
+    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
+    fflush(cm->stdOut);
+    sat_ReportStatistics(cm, cm->each);
+    sat_FreeManager(cm);
+  }
+  else if(cm->status == SAT_SAT) {
+    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
+    fflush(cm->stdOut);
+    sat_PrintSatisfyingAssignment(cm);
+    sat_ReportStatistics(cm, cm->each);
+    sat_FreeManager(cm);
+  }
+return cm->status;
+}
+/**Function********************************************************************
+ 
+  Synopsis    [Generate a CNF of the network]
+
+  Description [Generate the set of clauses of the unroll network for a given 
+  length and for a given cone of influence]
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+BmcCnfClauses_t*
+Dbg_GenerateCNF(Ntk_Network_t * network, 
+BmcOption_t * options,
+st_table  *CoiTable
+){
+st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
+BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
+/*
+ *nodeToMvfAigTable maps each node to its multi-function And/Inv graph
+ */
+nodeToMvfAigTable =
+(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+assert(nodeToMvfAigTable != NIL(st_table));
+/*
+ * Create a clause database
+ */
+cnfClauses = BmcCnfClausesAlloc();
+/*
+ * Generate clauses for an initialized path of length k
+ */
+BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
+			 cnfClauses, nodeToMvfAigTable, CoiTable);
+return cnfClauses;
+
+}
