src/bmc/bmcBmc.c

Go to the documentation of this file.

#include "bmcInt.h"

static char rcsid[] UNUSED = "$Id: bmcBmc.c,v 1.72 2005/10/14 04:41:11 awedh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int checkIndex(int index, BmcCnfClauses_t *cnfClauses);
static int doAnd(int left, int right);
static int doOr(int left, int right);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

void
BmcLtlVerifyProp(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  

  FILE              *cnfFile;

  array_t           *result = NIL(array_t);
  long              startTime, endTime;
  bAigEdge_t        property;
  array_t           *unitClause;
  
  assert(Ctlsp_isPropositionalFormula(ltlFormula));
  
  startTime = util_cpu_ctime();
  
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void) fprintf(vis_stdout, "LTL formula is propositional\n");
  }
  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
 
  if (property == mAig_NULL){
    return;
  }
  if (property == bAig_One){
    (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
    (void) fprintf(vis_stdout,"# BMC: formula failed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  } else if (property == bAig_Zero){
    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }
  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);    
  if (cnfFile == NIL(FILE)) {
    (void) fprintf(vis_stderr,
                   "** bmc error: Cannot create CNF output file %s\n",
                   options->satInFile);
    return;
  }
  /* 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 clauses database 
  */
  cnfClauses = BmcCnfClausesAlloc();
  unitClause = array_alloc(int, 1);

  /*
    Create an initialized path of length 0
   */
  BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
   
  /* Generate CNF for the property */
  array_insert(int, unitClause, 0,
               BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses));
  
  BmcCnfInsertClause(cnfClauses, unitClause);
  BmcWriteClauses(manager, cnfFile, cnfClauses, options);
  (void) fclose(cnfFile);

  result = BmcCheckSAT(options);
  if (options->satSolverError){
    (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
  } else {
    if (result != NIL(array_t)){
      (void) fprintf(vis_stdout, "# BMC: formula failed\n");
      if(options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,
                       "# BMC: Found a counterexample of length = 0 \n");
      }
      if (options->dbgLevel == 1) {
        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                               result, 0, CoiTable, options, NIL(array_t));
      }
      array_free(result);
    } else {
      if(options->verbosityLevel != BmcVerbosityNone_c){
        fprintf(vis_stdout,"# BMC: no counterexample found of length up to 0\n");
      }
      (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
    }
  }
  array_free(unitClause);   
  BmcCnfClausesFree(cnfClauses);
  
  if (options->verbosityLevel != BmcVerbosityNone_c){
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  fflush(vis_stdout);
  return;
} /* BmcLtlVerifyProp  */


int
BmcLtlCheckInductiveInvariant(
  Ntk_Network_t   *network,
  bAigEdge_t      property,
  BmcOption_t     *options,
  st_table        *CoiTable)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  array_t           *unitClause;
  int               cnfIndex;
  array_t           *result = NIL(array_t);
  FILE              *cnfFile;
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
  int               savedVerbosityLevel = options->verbosityLevel;
  int               returnValue = 0;  /* the property is not an inductive invariant */

  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);    
  if (cnfFile == NIL(FILE)) {
    (void) fprintf(vis_stderr,
                   "** bmc error: Cannot create CNF output file %s\n",
                   options->satInFile);
    return -1;
  }
  /*
    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));

  /*
    Clause database
   */
  cnfClauses = BmcCnfClausesAlloc();
  /*
    Check if the property holds in all intial states
  */
  /*
    Generate CNF clauses for initial states
  */
  BmcCnfGenerateClausesForPath(network, 0, 0, BMC_INITIAL_STATES,
                               cnfClauses, nodeToMvfAigTable, CoiTable);
  /*
    Generate CNF clauses for the property
  */
  cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
  unitClause = array_alloc(int, 1);
  array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
                                                the LTL formula*/
  BmcCnfInsertClause(cnfClauses, unitClause);
  
  options->verbosityLevel = BmcVerbosityNone_c;
  BmcWriteClauses(manager, cnfFile, cnfClauses, options);
  (void) fclose(cnfFile);
  result = BmcCheckSAT(options);    
  options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
  BmcCnfClausesFree(cnfClauses);
  if (options->satSolverError){
    return -1;
  }
  if (result == NIL(array_t)){ /* the property holds at all initial states */
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);    
    if (cnfFile == NIL(FILE)) {
      (void) fprintf(vis_stderr,
                     "** bmc error: Cannot create CNF output file %s\n",
                     options->satInFile);
      return -1;
    }
    /*
      Check if the property holds in state i, it also holds in state i+1
    */
    cnfClauses = BmcCnfClausesAlloc();  
    /*
      Generate CNF clauses for a transition from state i to state i+1.
    */
    BmcCnfGenerateClausesForPath(network, 0, 1, BMC_NO_INITIAL_STATES,
                                 cnfClauses, nodeToMvfAigTable, CoiTable);
    
    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 0, cnfClauses);
    array_insert(int, unitClause, 0, -cnfIndex); /* because property is the negation of
                                                    the LTL formula */
    BmcCnfInsertClause(cnfClauses, unitClause);
    
    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, 1, cnfClauses);
    array_insert(int, unitClause, 0, cnfIndex); /* because property is the negation of
                                                   the LTL formula */
    BmcCnfInsertClause(cnfClauses, unitClause);
    options->verbosityLevel = BmcVerbosityNone_c;
    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    result = BmcCheckSAT(options);
    options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
    BmcCnfClausesFree(cnfClauses);
    if (options->satSolverError){
      returnValue = -1;
    }
    if (result != NIL(array_t)){
      returnValue = 0; /* the property is not an inductive invariant */
    } else {
      returnValue = 1;  /* the property is an inductive invariant */
    }
  }
  array_free(unitClause);
  return returnValue; 
} /* BmcLtlCheckInductiveInvariant() */


void
BmcLtlVerifyGp(  
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  BmcCnfStates_t    *state;

  FILE              *cnfFile;
  array_t           *Pclause = array_alloc(int, 0);

  int               k, bound, initK, propK;
  array_t           *result = NIL(array_t);
  long              startTime, endTime;
  bAigEdge_t        property;
  int               minK = options->minK;
  int               maxK = options->maxK;
  int               i, initState = BMC_INITIAL_STATES;
  array_t           *unitClause;
  
  int               bmcError = FALSE;
  
  Bmc_PropertyStatus formulaStatus;
  
  assert(Ctlsp_LtlFormulaIsFp(ltlFormula));
  
  startTime = util_cpu_ctime();

  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void)fprintf(vis_stdout, "LTL formula is of type G(p)\n");
  }
  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);

  if (property == mAig_NULL){
    return;
  }
  if (property == bAig_One){
    (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
    (void) fprintf(vis_stdout,"# BMC: formula failed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  } else if (property == bAig_Zero){
    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }

#if 0
  if (options->verbosityLevel == BmcVerbosityMax_c){
    (void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
  }
  checkInductiveInvariant = BmcLtlCheckInductiveInvariant(network, property, options, CoiTable);
  
  if(checkInductiveInvariant == -1){
    return;
  }
  if (checkInductiveInvariant == 1){
    (void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }
#endif
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
                  minK, maxK, options->step);
  }
  initK  = 0;
  propK  = 0;
  formulaStatus = BmcPropertyUndecided_c;
  
  /* 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 clauses database 
  */
  cnfClauses = BmcCnfClausesAlloc();
  /*
    init = BmcCreateMaigOfInitialStates(network, nodeToMvfAigTable, CoiTable);
  */
  for(bound = minK; bound <= maxK; bound += options->step){
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout,
                     "\nBMC: Generate counterexample of length %d\n",
                     bound);
    }
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);    
    if (cnfFile == NIL(FILE)) {
      (void) fprintf(vis_stderr,
                     "** bmc error: Cannot create CNF output file %s\n",
                     options->satInFile);
      bmcError = TRUE;
      break;
    }
    BmcCnfGenerateClausesForPath(network, initK, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);

    initState = BMC_NO_INITIAL_STATES;
   
    /* Generate CNF for the property */
    Pclause = array_alloc(int, 0);
    /*
    state = BmcCnfClausesFreeze(cnfClauses);
    */
    for(k=propK; k <= bound; k++){
      array_insert_last(
        int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                          k, cnfClauses));
    }
    
    state = BmcCnfClausesFreeze(cnfClauses);
    
    BmcCnfInsertClause(cnfClauses, Pclause);
    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    BmcCnfClausesRestore(cnfClauses, state);
    result = BmcCheckSAT(options);
    if (options->satSolverError){
      array_free(Pclause);
      break;
    }
    if (result != NIL(array_t)){
      bound++;
      array_free(Pclause);
      /*
        formula failed\n"
      */
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    unitClause = array_alloc(int, 1);
    for(i=0; i<array_n(Pclause); i++){
      array_insert(int, unitClause, 0, -array_fetch(int, Pclause, i));
      BmcCnfInsertClause(cnfClauses, unitClause);
    }
    array_free(unitClause);   
    array_free(Pclause);
    FREE(state);
    initK = bound;
    propK = bound+1;

    /*
      Prove if the property passes using the induction proof of SSS0.
     */
    if((result == NIL(array_t)) &&
       (options->inductiveStep !=0) &&
       (bound % options->inductiveStep == 0)){
      BmcCnfClauses_t   *cnfClauses;
      array_t           *result = NIL(array_t);
      array_t           *unitClause =  array_alloc(int, 1);
      int               savedVerbosityLevel = options->verbosityLevel;
      long              startTime = util_cpu_ctime();
        
      if (options->verbosityLevel == BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout, "\nBMC: Check for induction\n");
      }
      options->verbosityLevel = BmcVerbosityNone_c;

      if(options->earlyTermination){
        /*
          Early termination condition
          
          Check if there is no simple path of length 'bound' starts from
          initial states
          
        */
        cnfClauses = BmcCnfClausesAlloc();
        
        cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
        if (cnfFile == NIL(FILE)) {
          (void)fprintf(vis_stderr,
                        "** bmc error: Cannot create CNF output file %s\n",
                        options->satInFile);
          bmcError = TRUE;
          break;
        }
        /*
          Generate an initialized simple path path of length bound.
        */
        BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
                                             cnfClauses, nodeToMvfAigTable, CoiTable);
        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
        (void) fclose(cnfFile);
        BmcCnfClausesFree(cnfClauses);
        
        result = BmcCheckSAT(options);
        if(options->satSolverError){
          break;
        }
        if(result == NIL(array_t)){
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout,
                           "# BMC: No simple path starting at an initial state\n");
          }
          formulaStatus = BmcPropertyPassed_c;
        } else {
          array_free(result);
        }
      } /* Early termination */
      if(formulaStatus != BmcPropertyPassed_c){
        cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
        if (cnfFile == NIL(FILE)) {
          (void)fprintf(vis_stderr,
                        "** bmc error: Cannot create CNF output file %s\n",
                        options->satInFile);
          bmcError = TRUE;
          break;
        }
        cnfClauses = BmcCnfClausesAlloc();
        /*
          Generate a simple path of length k+1
        */
        BmcCnfGenerateClausesForLoopFreePath(network, 0, bound+1, BMC_NO_INITIAL_STATES,
                                             cnfClauses, nodeToMvfAigTable, CoiTable);
        /*
          All the states to bound satisfy the property.
        */
        unitClause = array_alloc(int, 1);
        for(k=0; k <= bound; k++){
          array_insert(
            int, unitClause, 0, -BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                                     k, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
        }
        /*
          The property fails at bound +1
        */
        array_insert(int, unitClause, 0,
                     BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                         bound+1, cnfClauses));
        BmcCnfInsertClause(cnfClauses, unitClause);
        array_free(unitClause);
        
        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
        BmcCnfClausesFree(cnfClauses);
        (void) fclose(cnfFile);
        result = BmcCheckSAT(options);
        if (options->satSolverError){
          break;
        }
        if(result == NIL(array_t)) {
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout,
                           "# BMC: No simple path leading to a bad state\n");
          }
          formulaStatus = BmcPropertyPassed_c;
        }
      }
      options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
      if (options->verbosityLevel != BmcVerbosityNone_c){
        endTime = util_cpu_ctime();
        fprintf(vis_stdout, "-- check for induction time = %10g\n",
                (double)(endTime - startTime) / 1000.0);
      }
    } /* Check induction */
    if(formulaStatus != BmcPropertyUndecided_c){
      break;
    }
  } /* for bound loop */
  if( bmcError == FALSE){
    if (options->satSolverError){
      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
    } else {
      if(formulaStatus == BmcPropertyUndecided_c){
        if (options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: no counterexample found of length up to %d \n",
                         options->maxK);
        }
      }
      if(formulaStatus == BmcPropertyFailed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
         if(options->verbosityLevel != BmcVerbosityNone_c){
           (void) fprintf(vis_stdout,
                          "# BMC: Found a counterexample of length = %d \n", bound-1);
         }
        if (options->dbgLevel == 1) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, bound-1, CoiTable, options, NIL(array_t));
        }
      } else if(formulaStatus == BmcPropertyPassed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
      } else if(formulaStatus == BmcPropertyUndecided_c) {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
      }
    }
  }
  /* free all used memories */
  if(cnfClauses != NIL(BmcCnfClauses_t)){
    BmcCnfClausesFree(cnfClauses);
  }
  if(result != NIL(array_t)) {
    array_free(result);
  }
  /*
  array_free(Pclause);
  */
  if (options->verbosityLevel != BmcVerbosityNone_c){
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  fflush(vis_stdout);
  return;
} /* BmcLtlVerifyGp()  */

void
BmcLtlVerifyFp(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   BmcOption_t     *options)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  st_table        *nodeToMvfAigTable = NIL(st_table);  /* maps each node to its mvfAig */
  BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
  
  
  FILE       *cnfFile;
  array_t    *unitClause= array_alloc(int, 1), *outClause;
  int        outIndex;
  int        k;
  array_t    *result  = NIL(array_t);
  long       startTime, endTime;
  bAigEdge_t property;
  int        bound;
  int        bmcError = FALSE;
    
  Bmc_PropertyStatus formulaStatus = BmcPropertyUndecided_c;

  assert(Ctlsp_LtlFormulaIsGp(ltlFormula));
   
  startTime = util_cpu_ctime();
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void)fprintf(vis_stdout, "LTL formula is of type F(p)\n");
  }
  property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula->right);
  if (property == mAig_NULL){
    return;
  }
  if (property == bAig_One){
    (void) fprintf(vis_stdout, "# BMC: formula failed\n");
    (void) fprintf(vis_stdout, "       Empty counterexample because the property is always FALSE\n");
    if (options->verbosityLevel != BmcVerbosityNone_c) {
      endTime = util_cpu_ctime();
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(endTime - startTime) / 1000.0);
    }
    return;
  } else if (property == bAig_Zero){
    (void) fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
    formulaStatus = BmcPropertyPassed_c;
    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
    if (options->verbosityLevel != BmcVerbosityNone_c) {
      endTime = util_cpu_ctime();
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(endTime - startTime) / 1000.0);
    }
    return;
  }
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void)fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  options->minK, options->maxK, options->step);
  }
  /*
    nodeToMvfAigTable Maps each node to its Multi-function AIG graph
  */
  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));
  outClause = NIL(array_t);
  bound = options->minK;
  BmcGetCoiForLtlFormula(network, ltlFormula, CoiTable);
  
  while( (result == NIL(array_t)) && (bound <= options->maxK)){
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout,
                     "\nBMC: Generate counterexample of length %d\n", bound);
    }
    cnfClauses = BmcCnfClausesAlloc();
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);    
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      bmcError = TRUE;
      break;
    }
    /*
      Generate clauses for an initialized path of length "bound".
    */
    BmcCnfGenerateClausesForPath(network, 0, bound, BMC_INITIAL_STATES,
                                 cnfClauses, nodeToMvfAigTable, CoiTable);
    /*
      Generate CNF for the property. Property fails at all states
     */
    for(k=0; k <= bound; k++){
      array_insert(int, unitClause, 0,
                   BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                       k, cnfClauses));
      BmcCnfInsertClause(cnfClauses, unitClause);
    }

    /* Generate CNF for a loop-back (loop from the last state to any
       state) path.
       (Sk -> S0) + (Sk -> S1) + ..... + (Sk-> Sk-1) + (Sk-> Sk)
       Each transition consisits of one or more latches.  We
       AND the transiton relation of these latches.  For multi-valued
       latches, we OR the equivalence of each value of the latch. To
       do the AND we use the CNF equivalent of the AND.  a = b*c => (b
       + !a) * (c + !a)
    */
    outClause = array_alloc(int, bound);   
    for (k=0; k <= bound; k++){
      /*
        Create new var for the output of the AND node.
      */
      outIndex = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesFromStateToState(network, bound, k, cnfClauses,
                                            nodeToMvfAigTable, CoiTable, outIndex);
      array_insert(int, outClause, k, outIndex);
    }  /* for k state loop */
    BmcCnfInsertClause(cnfClauses, outClause);
  
    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
    
    result = BmcCheckSAT(options);
    if (options->satSolverError){
      break;
    }
    if(result != NIL(array_t)){
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    BmcCnfClausesFree(cnfClauses);
    array_free(outClause);
    if((result == NIL(array_t)) &&
       (options->inductiveStep !=0) &&
       (bound % options->inductiveStep == 0)
       )    
      {
      int     savedVerbosityLevel = options->verbosityLevel;
      long    startTime = util_cpu_ctime();
      array_t *result  = NIL(array_t);

      if (options->verbosityLevel == BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout,
                       "\nBMC: Check if the property passes\n");
      }
      cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
      if (cnfFile == NIL(FILE)) {
        (void)fprintf(vis_stderr,
                      "** bmc error: Cannot create CNF output file %s\n",
                      options->satInFile);
        bmcError = TRUE;
        break;
      }
      cnfClauses = BmcCnfClausesAlloc();
      /*
        CNF for an initialized simple path.
       */
      BmcCnfGenerateClausesForLoopFreePath(network, 0, bound, BMC_INITIAL_STATES,
                                           cnfClauses, nodeToMvfAigTable, CoiTable);
      /*
        Generate CNF for the property. Property fails at all states
      */
      for(k=0; k <= bound; k++){
        array_insert(int, unitClause, 0,
                     BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                         k, cnfClauses));
        BmcCnfInsertClause(cnfClauses, unitClause);
      }
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      BmcCnfClausesFree(cnfClauses);
      (void) fclose(cnfFile);
      /*
        Do not print any detail information when checking the clauses
       */
      options->verbosityLevel = BmcVerbosityNone_c;
      result = BmcCheckSAT(options);
      options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
      if (options->satSolverError){
        break;
      }
      if (options->verbosityLevel != BmcVerbosityNone_c){
        endTime = util_cpu_ctime();
        fprintf(vis_stdout, "--  checking time = %10g\n",
                (double)(endTime - startTime) / 1000.0);
      }
      if (result == NIL(array_t)){ /* UNSAT */
        formulaStatus = BmcPropertyPassed_c;
        break;  /* formula is satisfiable */
      }
      array_free(result);
    } /* Check induction */

    /* free all used memories 
    BmcCnfClausesFree(cnfClauses); */

    bound += options->step;
  } /* while result and bound */
  if (bmcError == FALSE){
    if(!options->satSolverError){
      if(formulaStatus == BmcPropertyFailed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
        if(options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: Found a counterexample of length = %d \n", bound);
        }
        if (options->dbgLevel == 1) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, bound, CoiTable, options, outClause);
        }
        array_free(result);
        BmcCnfClausesFree(cnfClauses);
        array_free(outClause);
      } else if(formulaStatus == BmcPropertyPassed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
      } else if(formulaStatus == BmcPropertyUndecided_c) {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
        if (options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                       "# BMC: no counterexample found of length up to %d \n",
                         options->maxK);
        }
      }
    } else {
      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
    }
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  if(unitClause != NIL(array_t)) {
    array_free(unitClause);
  }
  fflush(vis_stdout);  
  return;
} /* BmcLtlVerifyFp() */

void
BmcLtlVerifyFGp(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   BmcOption_t     *options)
{
  mAig_Manager_t   *manager = Ntk_NetworkReadMAigManager(network);
  st_table         *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
  BmcCnfClauses_t  *cnfClauses = NIL(BmcCnfClauses_t);
  FILE             *cnfFile;
  
  array_t          *orClause, *tmpClause, *loopClause;
  int              k, l, andIndex, loop;
  array_t          *result = NIL(array_t);
  long             startTime, endTime;
  int              minK = options->minK;
  int              maxK = options->maxK;
  Ctlsp_Formula_t  *propFormula;
  bAigEdge_t       property;

  Bmc_PropertyStatus formulaStatus;
  int                bmcError = FALSE;
  
  int              m=-1, n=-1;
  int              checkLevel = 0;
  /*
    Refer to Theorem 1 in the paper "Proving More Properties with Bounded Model Checking"
    
    If checkLevel == 0 -->  check for beta' only. If UNSAT, m=k and chekLevel = 1
    If checkLevel == 1 -->  check for beta  only. If UNSAT, checkLevel = 2.
    If checkLevel == 2 -->  check for alpha only. If UNSAT, n=k and checkLevel = 3.
    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
    checkLevel = 4 if (m+n-1) > maxK; */

  /*
    Remember the LTL property was negated
   */
  assert(Ctlsp_LtlFormulaIsGFp(ltlFormula));

  /* ************** */
  
  /* Initialization */
  
  /* ************** */
  loopClause = NIL(array_t);
  startTime = util_cpu_ctime();
  /*
    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
  */
  nodeToMvfAigTable =
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    (void) fprintf(vis_stderr,
                   "** bmc error: you need to build the AIG structure first\n");
    return;
  }
  propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
  property    = BmcCreateMaigOfPropFormula(network, manager, propFormula);
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void)fprintf(vis_stdout, "LTL formula is of type FG(p)\n");
    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  minK, maxK, options->step);
  }
  tmpClause  = array_alloc(int, 2);
  k= minK;
  formulaStatus = BmcPropertyUndecided_c;
  while( (result == NIL(array_t)) && (k <= maxK)){
    /*
      Search for a k-loop counterexample of length k.
     */
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }
    /*
      Create a clause database
     */
    cnfClauses = BmcCnfClausesAlloc();

    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      bmcError = TRUE;
      break;
    }
    
    /**********************************************
       \gama(k)
    ***********************************************/
    /*
      Generate an initialized path of length k.
     */
    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, CoiTable);
    /*
      k-loop
     */
    orClause   = array_alloc(int, 0);
    loopClause = array_alloc(int, k+1);
    for(l=0; l<=k; l++){
      /*
        Use to check if there is a loop from k to l.
       */
      loop = cnfClauses->cnfGlobalIndex++;
      BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses, nodeToMvfAigTable, CoiTable, loop);
      array_insert(int, loopClause, l, loop);
      
      andIndex   = cnfClauses->cnfGlobalIndex++;
      array_insert(int, tmpClause, 0, loop);
      array_insert(int, tmpClause, 1, -andIndex);
      BmcCnfInsertClause(cnfClauses, tmpClause);

      /*
                 l
        If [[F p]]  if p true in a state from l to k.
                 k
       */
      array_insert(int, tmpClause, 0,
                   BmcGenerateCnfForLtl(network, Ctlsp_FormulaCreate(Ctlsp_F_c, propFormula, NIL(Ctlsp_Formula_t)),
                                        l, k, -1, cnfClauses));
      BmcCnfInsertClause(cnfClauses, tmpClause);
      
      array_insert_last(int, orClause, andIndex);
    } /* for l loop */
    BmcCnfInsertClause(cnfClauses, orClause);
    array_free(orClause);
    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    (void) fclose(cnfFile);
      
    result = BmcCheckSAT(options);
    if(options->satSolverError){
      break;
    }
    if(result != NIL(array_t)) {
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    array_free(loopClause);
    /* free all used memories */
    BmcCnfClausesFree(cnfClauses);

    /* ====================================================================
             Use termination criteria to prove that the property passes.
       ==================================================================== */
    if((result == NIL(array_t)) &&
       (options->inductiveStep !=0) &&
       (k % options->inductiveStep == 0)
       )
      {
        array_t *unitClause = array_alloc(int, 0);
        array_t *result = NIL(array_t);
        int     savedVerbosityLevel = options->verbosityLevel;

        options->verbosityLevel = BmcVerbosityNone_c;
        /* ===========================
           Early termination condition
           =========================== */
        if(options->earlyTermination){
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
          }
          cnfClauses = BmcCnfClausesAlloc();

          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
          if (cnfFile == NIL(FILE)) {
            (void)fprintf(vis_stderr,
                          "** abmc error: Cannot create CNF output file %s\n",
                          options->satInFile);
            bmcError = TRUE;
            break;
          }
          /*
            Generate an initialized simple path path of length k.
          */
          BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
                                               cnfClauses, nodeToMvfAigTable, CoiTable);
          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
          (void) fclose(cnfFile);
          BmcCnfClausesFree(cnfClauses);
          
          result = BmcCheckSAT(options);
          if(options->satSolverError){
            break;
          }
          if(result == NIL(array_t)) {
            formulaStatus = BmcPropertyPassed_c;
            if (savedVerbosityLevel == BmcVerbosityMax_c) {
              (void) fprintf(vis_stdout, "# BMC: By early termination\n");
            }
            break;
          }
        } /* Early termination */

        /*
          Check \beta''(k)
        */
        if(checkLevel == 0){
          int i;
          
          cnfClauses = BmcCnfClausesAlloc();
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check beta'' \n");
          }
          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
          if (cnfFile == NIL(FILE)) {
            (void)fprintf(vis_stderr,
                          "** bmc error: Cannot create CNF output file %s\n",
                          options->satInFile);
            bmcError = TRUE;
            break;
          }
          /*
            Generate a simple path of length k+1.
          */
          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
                                               cnfClauses, nodeToMvfAigTable, CoiTable);
          for(i=1; i<=k+1; i++){
            array_insert(int, unitClause, 0,
                         -BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                              i, cnfClauses));
            BmcCnfInsertClause(cnfClauses, unitClause);
          }
          array_insert(int, unitClause, 0,
                       BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                           0, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
          
          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
          (void) fclose(cnfFile);
          
          result = BmcCheckSAT(options);
          BmcCnfClausesFree(cnfClauses);
          if(options->satSolverError){
            break;
          }
          if(result == NIL(array_t)) {
            m = k;
            printf("Beta'': Value of m = %d\n", m);
            checkLevel = 1;
          }
        } /* Check for beta'' */
        
        /*
          Check \beta'(k) 
        */
        if(checkLevel == 0){
          int i;
          
          cnfClauses = BmcCnfClausesAlloc();
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check beta' \n");
          }
          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
          if (cnfFile == NIL(FILE)) {
            (void)fprintf(vis_stderr,
                          "** bmc error: Cannot create CNF output file %s\n",
                          options->satInFile);
            bmcError = TRUE;
            break;
          }
          /*
            Generate a simple path of length k+1.
          */
          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
                                               cnfClauses, nodeToMvfAigTable, CoiTable);
          for(i=0; i<=k; i++){
            array_insert(int, unitClause, 0,
                         -BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                              i, cnfClauses));
            BmcCnfInsertClause(cnfClauses, unitClause);
          }
          array_insert(int, unitClause, 0,
                       BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                           k+1, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
          
          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
          (void) fclose(cnfFile);
          
          result = BmcCheckSAT(options);
          BmcCnfClausesFree(cnfClauses);
          if(options->satSolverError){
            break;
          }
          if(result == NIL(array_t)) {
            m = k;
            printf("Beta': Value of m = %d\n", m);
            checkLevel = 1;
          }
        } /* Check for beta' */
        /*
          Check for beta
        */
        if(checkLevel == 1){
          cnfClauses = BmcCnfClausesAlloc();
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check beta\n");
          }       
          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
          if (cnfFile == NIL(FILE)) {
            (void)fprintf(vis_stderr,
                          "** bmc error: Cannot create CNF output file %s\n",
                          options->satInFile);
            bmcError = TRUE;
            break;
          }
          /*
            Generate a simple path of length k+1.
          */
          BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
                                               cnfClauses, nodeToMvfAigTable, CoiTable);
          array_insert(int, unitClause, 0,
                       -BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                            k, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
          array_insert(int, unitClause, 0,
                       BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                           k+1, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
          
          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
          (void) fclose(cnfFile);
          
          result = BmcCheckSAT(options);
          BmcCnfClausesFree(cnfClauses);
          if(options->satSolverError){
            break;
          }
          if(result == NIL(array_t)) {
            checkLevel = 2;
          }
        } /* Check beta */
      
        if(checkLevel == 2){ /* we check \alpha if \beta UNSAT */
          if (savedVerbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check alpha \n");
          }       
          /*
            \alpha(k)
          */
          cnfClauses = BmcCnfClausesAlloc();
         
          cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
          if (cnfFile == NIL(FILE)) {
            (void)fprintf(vis_stderr,
                          "** bmc error: Cannot create CNF output file %s\n",
                          options->satInFile);
            bmcError = TRUE;
            break;
          }
          /*
            Generate an initialized path of length k.
          */
          BmcCnfGenerateClausesForLoopFreePath(network, 0, k, BMC_INITIAL_STATES,
                                               cnfClauses, nodeToMvfAigTable, CoiTable);
          
          array_insert(int, unitClause, 0,
                       BmcGenerateCnfFormulaForAigFunction(manager, property,
                                                           k, cnfClauses));
          BmcCnfInsertClause(cnfClauses, unitClause);
          
          
          BmcWriteClauses(manager, cnfFile, cnfClauses, options);
          (void) fclose(cnfFile);
          
          result = BmcCheckSAT(options);
          BmcCnfClausesFree(cnfClauses);
          if(options->satSolverError){
            break;
          }
          if(result == NIL(array_t)) {
            n = k;
            checkLevel = 3;
            printf("m=%d  n=%d\n",m,n);
            if ((m+n-1) <= maxK){
              maxK = m+n-1;
            } else {
              checkLevel = 4;
            }
          }
        }/* Check alpha */
        array_free(unitClause);
        options->verbosityLevel = (Bmc_VerbosityLevel) savedVerbosityLevel;
      } /* Prove the property passes*/
    k += options->step;
  } /* while result and k*/
  if (bmcError == FALSE){
    if(options->satSolverError){
      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
    } else {
      if(checkLevel == 3){
        (void) fprintf(vis_stdout, "# BMC: (m+n-1) Complete the theorem\n");
        formulaStatus = BmcPropertyPassed_c;
      }
      if(formulaStatus == BmcPropertyFailed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
        if(options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: Found a counterexample of length = %d \n", k);
        }
        if (options->dbgLevel == 1) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, k, CoiTable, options, loopClause);
          BmcCnfClausesFree(cnfClauses);
          array_free(loopClause);
        }
      } else if(formulaStatus == BmcPropertyPassed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
      } else if(formulaStatus == BmcPropertyUndecided_c) {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
        if (options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: no counterexample found of length up to %d \n",
                         maxK);
        }
      }
    }
  }
  /*
    free all used memories
  */
  array_free(tmpClause);
 
  if(result != NIL(array_t)){
    array_free(result);
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- abmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  fflush(vis_stdout);
  return;
} /* BmcLtlVerifyGFp() */

void
BmcLtlVerifyUnitDepth(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  FILE              *cnfFile;

  array_t           *orClause =NIL(array_t);
  array_t           *loopClause, *tmpclause;
  int               l, loopIndex, andIndex, loop;
  int               noLoopIndex;
  array_t           *result = NIL(array_t);
  
  int               leftValue  = 0;
  int               rightValue = 0;
  long              startTime, endTime;
  int               k;
  int               minK = options->minK;
  int               maxK = options->maxK;
                    /* Store the index of a loop from k to all sate from 0 to k */
  
  Bmc_PropertyStatus       formulaStatus;
  BmcCheckForTermination_t *terminationStatus = 0;
  int                      bmcStatus=0; /* Holds the status of running BMC
                                           = -1 if there is an error */
  
  assert(Ctlsp_LtlFormulaDepth(ltlFormula) == 1);
  
  /* ************** */
  /* Initialization */
  /* ************** */
  
  startTime = util_cpu_ctime();
  /*
    nodeToMvfAigTable maps each node to its multi-function AIG graph
  */
  nodeToMvfAigTable =
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));

  loopClause = NIL(array_t);
  
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void) fprintf(vis_stdout, "Unit depth LTL formula\n");
    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  minK, maxK, options->step);
  }
   if(options->inductiveStep !=0){
     /*
       Use the termination criteria to prove the property passes.    
     */
     terminationStatus = BmcAutTerminationAlloc(network,
                                                Ctlsp_LtllFormulaNegate(ltlFormula),
                                                NIL(array_t));
     assert(terminationStatus);
   }
  k = minK;
  formulaStatus = BmcPropertyUndecided_c;
  while( (result == NIL(array_t)) && (k <= maxK)){
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }
    /*
      Create clause database
     */
    cnfClauses = BmcCnfClausesAlloc();

    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      bmcStatus = -1;
      break;
    }
    /*
      Generate clauses represent an initialized path of length k
     */
    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
                                 cnfClauses, nodeToMvfAigTable, CoiTable);
    /*
      Generate clauses represent paths which satisfy the LTL formula if
      there is no loop.
    */
    noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
    leftValue   = checkIndex(noLoopIndex, cnfClauses);
    if (leftValue != 1) { /* no loop  part of the basic encoding is not TRUE */
      orClause = array_alloc(int, 0);   
      /*
        No need to check for !Lk in the basic encoding 
      */
      if (leftValue == -1){ /* no loop part of the basic encoding is not FALSE */
        array_insert_last(int, orClause, noLoopIndex);
      }
      /*
        Generate clauses represent paths which satisfy the LTL formula if
        there is a loop.
      */
      loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, 0, cnfClauses);
      rightValue = checkIndex(loopIndex, cnfClauses);
      if (rightValue == 0){ /* loop  part of the basic encoding is FALSE */
        break;
      }
      /*
        rightValue can be 1 or -1
        leftValue can be 0 or -1
       */
      if (noLoopIndex == loopIndex){ /* do not check for the existence of a loop*/
        break;
      }
      /*
        Clauses for loop-back path.
       */
      loopClause = array_alloc(int, k+2);
      for(l=0; l<=k; l++){
          loop = cnfClauses->cnfGlobalIndex++;
          BmcCnfGenerateClausesFromStateToState(network, k, l, cnfClauses,
                                                nodeToMvfAigTable, CoiTable, loop);
          array_insert(int, loopClause, l, loop);
      } /* for l loop */
      loop = cnfClauses->cnfGlobalIndex++;
      array_insert(int, loopClause, k+1, -loop);
      BmcCnfInsertClause(cnfClauses, loopClause);
      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);
      }
    }
    /* if((leftValue == 1) || (rightValue == 1)){ */
    if(leftValue == 1){
      assert(k==1);
      /*
        formula failed
      */
      formulaStatus = BmcPropertyFailed_c;
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
      }
      break;
    } else if((leftValue == 0) && (rightValue == 0)){
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
      }
    } else {
      BmcCnfInsertClause(cnfClauses, orClause);
      array_free(orClause);
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      (void) fclose(cnfFile);
      
      result = BmcCheckSAT(options);
      if(options->satSolverError){
        break;
      }
      if(result != NIL(array_t)) {
        /*
          formula failed
        */
        formulaStatus = BmcPropertyFailed_c;
      } else {
        /* free some used memories */
        BmcCnfClausesFree(cnfClauses);
        array_free(loopClause);
        /*
          Use the termination check
        */

        if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
          if((options->inductiveStep !=0) &&
             (k % options->inductiveStep == 0)
             )
            {
              /*
                Check for termination for the current value of k.
              */
              terminationStatus->k = k;
              bmcStatus = BmcAutLtlCheckForTermination(network,
                                                       NIL(array_t), terminationStatus,
                                                       nodeToMvfAigTable, CoiTable, options);
              if(bmcStatus == 1){
                maxK = options->maxK;
              }
              if(bmcStatus == 3){
                formulaStatus = BmcPropertyPassed_c;
                break;
              }
              if(bmcStatus == -1){
                break;
              }
            }
        } /* terminationStatus */
      }
    }
    k += options->step;
  } /* while result and k*/

 /*
    If no error.
   */
  if(bmcStatus != -1){
    if(bmcStatus == 1){
      (void) fprintf(vis_stdout,
                     "# BMC: no counterexample found of length up to %d \n", options->maxK);
      (void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
      formulaStatus = BmcPropertyPassed_c;
    }
    if(options->satSolverError){
      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
    } else {
      if(formulaStatus == BmcPropertyFailed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
        if(options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: Found a counterexample of length = %d \n", k);
        }
        if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, k, CoiTable, options, loopClause);
        }
        /* free some used memories */
        BmcCnfClausesFree(cnfClauses);
        array_free(loopClause);
        array_free(result);
      } else if(formulaStatus == BmcPropertyPassed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
        (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
      } else if(formulaStatus == BmcPropertyUndecided_c) {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
        if (options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: no counterexample found of length up to %d \n",
                         maxK);
        }
      }
    }
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  if(terminationStatus){
    BmcAutTerminationFree(terminationStatus);
  }
  fflush(vis_stdout);
  return;
} /* Bmc_VerifyUnitDepth() */

void
BmcLtlVerifyGeneralLtl(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   st_table        *CoiTable,
   array_t         *constraintArray,
   BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  FILE              *cnfFile;

  array_t           *orClause = NIL(array_t);
  array_t           *loopClause, *tmpclause;
  int               l, loopIndex, andIndex, loop;
  int               noLoopIndex;
  array_t           *result = NIL(array_t);
  array_t           *fairnessArray = NIL(array_t);
  int               leftValue  = 0;
  int               rightValue = 0;
  long              startTime, endTime;
  int               k;
  int               minK = options->minK;
  int               maxK = options->maxK;
  boolean           boundedFormula;
  int               depth;
                    /* Store the index of loop from k to all sate from 0 to k */
  
  array_t           *ltlConstraintArray;        /* constraints converted to LTL */
  int               f;
  boolean           fairness  = (constraintArray != NIL(array_t));

  BmcCheckForTermination_t *terminationStatus = 0;
  Bmc_PropertyStatus       formulaStatus;
  int                      bmcStatus=0; /* Holds the status of running BMC
                                           = -1 if there is an error */
  
  /* ************** */
  /* Initialization */
  /* ************** */
  startTime = util_cpu_ctime();
  /*
    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));

  loopClause = NIL(array_t);
  noLoopIndex = 0;
  ltlConstraintArray = NIL(array_t);
  if(fairness){
    Ctlsp_Formula_t *formula;
    int              i;
    /*
      All formulae in constraintArray are propositional, propositional
      constraint.
    */
    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
      /*
        To help making propositional constraint easy to encode.
      */
      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
      array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
      BmcGetCoiForLtlFormula(network, formula, CoiTable);
    }
  }
  /*
    For bounded formulae use a tighter upper bound if possible.
  */
  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
  if (boundedFormula && depth < maxK && depth >= minK) {
    maxK = depth;
  } else {
    if(options->inductiveStep !=0){
      /*
        Use the termination criteria to prove the property passes.    
      */
      terminationStatus = BmcAutTerminationAlloc(network,
                                                 Ctlsp_LtllFormulaNegate(ltlFormula),
                                                 constraintArray);
      assert(terminationStatus);
    }
  }
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void) fprintf(vis_stdout, "General LTL BMC\n");
    if (boundedFormula){
      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
    }
    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  minK, maxK, options->step);
  }
  k= minK;
  formulaStatus = BmcPropertyUndecided_c;
  while( (result == NIL(array_t)) && (k <= maxK)){
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }

    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      bmcStatus = -1;
      break;
    }
    /*
      Create a clause database
     */
    cnfClauses = BmcCnfClausesAlloc();
    /*
      Gnerate clauses for an initialized path of length k
     */
    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
                                 cnfClauses, nodeToMvfAigTable, CoiTable);

    if(!fairness){ /* No fairness constraint */
      noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
      leftValue   = checkIndex(noLoopIndex, cnfClauses);
    } else {
      leftValue = 0; /* the path must have a loop*/
    }
    if (leftValue != 1) {
      orClause = array_alloc(int, 0);   
      /*
        No need to check for !Lk in the basic encoding 
      */
      if (leftValue == -1){
        array_insert_last(int, orClause, noLoopIndex);
      }
      loopClause = array_alloc(int, k+1);
     
      for(l=0; l<=k; l++){
        loopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, l, cnfClauses);
        rightValue = checkIndex(loopIndex, cnfClauses);
        if (rightValue == 0){
          break;
        }
        if(fairness){
          Ctlsp_Formula_t *formula;
          int             i;

          fairnessArray = array_alloc(int, 0);
          arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
            array_insert_last(int, fairnessArray,
                              BmcGenerateCnfForLtl(network, formula, l, k, -1, cnfClauses));
          }
        }
        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);
            
            if(fairness){
              for(f=0; f < array_n(fairnessArray); f++){
                array_insert(int, tmpclause, 0, array_fetch(int, fairnessArray, f)); 
                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);
          }
        }
        if(fairness){
          array_free(fairnessArray);
        }
      } /* for l loop */
    }
    if((leftValue == 1) || (rightValue == 1)){
      assert(k==1);
      if (options->verbosityLevel != BmcVerbosityNone_c){
        formulaStatus = BmcPropertyFailed_c;
        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
      }
      break;
    } else if((leftValue == 0) && (rightValue == 0)){
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
      }
    } else {
      /*
      BmcCnfInsertClause(cnfClauses, loopClause);
      */
      BmcCnfInsertClause(cnfClauses, orClause);
      /*
      array_free(loopClause);
      */
      array_free(orClause);
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      (void) fclose(cnfFile);
      
      result = BmcCheckSAT(options);
      if(options->satSolverError){
        break;
      }
      if(result != NIL(array_t)) {
        /*
          formula failed\n"
         */
        formulaStatus = BmcPropertyFailed_c;
        break;
      }
      array_free(loopClause);
    }
    /* free all used memories */
    BmcCnfClausesFree(cnfClauses);
    cnfClauses = NIL(BmcCnfClauses_t);
    
    /*
      Use the termination check if the the LTL formula is not bounded
     */
    if(terminationStatus && (formulaStatus == BmcPropertyUndecided_c) && (bmcStatus != 1)){
      if((options->inductiveStep !=0) &&
         (k % options->inductiveStep == 0)
         )
        {
          /*
            Check for termination for the current value of k.
           */
          terminationStatus->k = k;
          bmcStatus = BmcAutLtlCheckForTermination(network,
                                                   constraintArray, terminationStatus,
                                                   nodeToMvfAigTable, CoiTable, options);
          if(bmcStatus == 1){
            maxK = terminationStatus->k;
          }
          if(bmcStatus == 3){
            formulaStatus = BmcPropertyPassed_c;
            break;
          }
          if(bmcStatus == -1){
            break;
          }
        }
    } /* terminationStatus */
    k += options->step;
  } /* while result and k*/

  /*
    If no error.
   */
  if(bmcStatus != -1){
    /*
    if(result == NIL(array_t)){
    */
    if(formulaStatus == BmcPropertyUndecided_c){
      if(bmcStatus == 1){
        (void) fprintf(vis_stdout,
                       "# BMC: no counterexample found of length up to %d \n", maxK);
        (void) fprintf(vis_stdout, "# BMC: By termination criterion (m+n-1)\n");
        formulaStatus = BmcPropertyPassed_c;
      }
      if (boundedFormula && depth <= options->maxK){
        (void) fprintf(vis_stdout,
                       "# BMC: no counterexample found of length up to %d \n", depth);
        formulaStatus = BmcPropertyPassed_c;
      }
    }
    if(options->satSolverError){
      (void) fprintf(vis_stdout,"# BMC: Error in calling SAT solver\n");
    } else {
      if(formulaStatus == BmcPropertyFailed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
        if(options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: Found a counterexample of length = %d \n", k);
        }
        if ((options->dbgLevel == 1) && (result != NIL(array_t))) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, k, CoiTable, options, loopClause);
        }
        /*BmcCnfClausesFree(cnfClauses);*/
        array_free(loopClause);
      } else if(formulaStatus == BmcPropertyPassed_c) {
        (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
        (void) fprintf(vis_stdout, "#      Termination depth = %d\n", maxK);
      } else if(formulaStatus == BmcPropertyUndecided_c) {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
        if (options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: no counterexample found of length up to %d \n",
                         maxK);
        }
      }
    }
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  /*
    free all used memories
  */
  if(terminationStatus){
    BmcAutTerminationFree(terminationStatus);
  }
  if(result != NIL(array_t)){
    array_free(result);
  }
  if(cnfClauses != NIL(BmcCnfClauses_t)){
    BmcCnfClausesFree(cnfClauses);
  }
  if(fairness){
    /*Ctlsp_FormulaArrayFree(ltlConstraintArray);*/
  }
  fflush(vis_stdout);
  return;
} /* BmcLtlVerifyGeneralLtl() */

int
BmcGenerateCnfForLtl(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   int             i /* from state i */,
   int             k /* to state k   */,
   int             l /* loop         */,
   BmcCnfClauses_t *cnfClauses)
{
  int left, right, cnfIndex;
  int andIndex, orIndex;
  int j, n;
  int leftValue, rightValue, andValue, orValue;
  
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  array_t         *clause, *tmpclause, *orClause, *rightClause, *leftClause;
  BmcCnfStates_t  *state;
  
  assert(ltlFormula != NIL(Ctlsp_Formula_t));
  right = 0;
  rightValue = 0;
  
  if(Ctlsp_isPropositionalFormula(ltlFormula)){
    bAigEdge_t property = BmcCreateMaigOfPropFormula(network, manager, ltlFormula);
       
    if (property == bAig_Zero){ /* FALSE */
      /* add an empty clause to indicate FALSE property */
      BmcAddEmptyClause(cnfClauses);
      return 0;
    }
    if (property == bAig_One){ /* TRUE */
      /* Don't generate any clause to indicate TRUE property.*/
      return 0;
    }
    /* Generate the clause of the propositional formula */
    /* The state of the input variables is the same as the state of the state variables. */
    cnfIndex = BmcGenerateCnfFormulaForAigFunction(manager, property, i, cnfClauses);    
    return cnfIndex;
  }
  /*
   * Formula is NOT propositional formula 
   */
  switch(ltlFormula->type) {
    case Ctlsp_NOT_c:
      /* reach here if formula-left is always not propositional*/
      /* NOT must only appears infront of a propositional formula.*/
      if (!Ctlsp_isPropositionalFormula(ltlFormula->left)){
        fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
        return 0;
      }
      /*
      return -1*BmcGenerateCnfForLtlNoLoop(network, ltlFormula->left, i, k,
                                           cnfIndexTable, clauseArray);
      */
      break;
    case Ctlsp_AND_c:
      /*
          c = a * b  -->  (!a + !b + c) * (a + !c) * (b + !c).
          Because a and b must be one, so we need only the last two clauses.
       */
      
      state = BmcCnfClausesFreeze(cnfClauses);
      rightValue = 1;
      
      left      = BmcGenerateCnfForLtl(network, ltlFormula->left,  i, k, l, cnfClauses);
      leftValue = checkIndex(left, cnfClauses);

      if (leftValue !=0){
        right      = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
        rightValue = checkIndex(right, cnfClauses);
      }
      if ((leftValue == 0) || (rightValue == 0)){
        /* restore the information */
        BmcCnfClausesRestore(cnfClauses, state);
        /* add an empty clause*/
        BmcAddEmptyClause(cnfClauses);
        FREE(state);
        return 0;  /* FALSE */
      }
      if ((leftValue == 1) && (rightValue == 1)){
        /* restore the information */
        BmcCnfClausesRestore(cnfClauses, state);
        FREE(state);
        return 0; /* TRUE */
      }
      BmcCnfClausesUnFreeze(cnfClauses, state);
      FREE(state);
      /*
      tmpclause  = array_alloc(int, 3);
      array_insert(int, tmpclause, 0, -left);
      array_insert(int, tmpclause, 1, -right);
      array_insert(int, tmpclause, 2,  cnfIndex);
      array_insert_last(array_t *, clauseArray, tmpclause);
      */
      if (leftValue == 1){
        return right;
      }
      if (rightValue == 1){
        return left;
      }
      cnfIndex = cnfClauses->cnfGlobalIndex++;      
      tmpclause  = array_alloc(int, 2);
      
      array_insert(int, tmpclause, 0, left);
      array_insert(int, tmpclause, 1, -cnfIndex);
      BmcCnfInsertClause(cnfClauses, tmpclause);
      
      array_insert(int, tmpclause, 0, right);
      array_insert(int, tmpclause, 1, -cnfIndex);
      BmcCnfInsertClause(cnfClauses, tmpclause);
      array_free(tmpclause);

      return cnfIndex;
    case Ctlsp_OR_c:
      /*
          c = a + b  -->  (a + b + !c) * (!a + c) * (!b + c).
          Because a and b must be one, so we need only the first clause.
       */
      state = BmcCnfClausesFreeze(cnfClauses);
            
      left      = BmcGenerateCnfForLtl(network, ltlFormula->left,  i, k, l, cnfClauses);
      leftValue = checkIndex(left, cnfClauses);

      if (leftValue !=1){
        right      = BmcGenerateCnfForLtl(network, ltlFormula->right, i, k, l, cnfClauses);
        rightValue = checkIndex(right, cnfClauses);
      }
      if ((leftValue == 1) || (rightValue == 1)){
        /* restore the information */
        BmcCnfClausesRestore(cnfClauses, state);
        FREE(state);
        return 0;  /* TRUE */
      } 
      if ((leftValue == 0) && (rightValue == 0)){
        /* restore the information */
        BmcCnfClausesRestore(cnfClauses, state);
        /* add an empty clause*/
        BmcAddEmptyClause(cnfClauses);
        FREE(state);
        return 0;  /* FALSE */
      }
      BmcCnfClausesUnFreeze(cnfClauses, state);
      FREE(state);
      /* Either leftValue or rightValue = 0 and the other != 1
         At least one clause will be added
       */
      if (leftValue == 0){
        return right;
      }
      if (rightValue == 0){
        return left;
      }      
      cnfIndex = cnfClauses->cnfGlobalIndex++;

      tmpclause  = array_alloc(int, 0);
      array_insert_last(int, tmpclause, -cnfIndex);
      
      array_insert_last(int, tmpclause, left);
        /*
        tmpclause  = array_alloc(int, 2);
        array_insert(int, tmpclause, 0, -left);
        array_insert(int, tmpclause, 1, cnfIndex);
        array_insert_last(array_t *, clauseArray, tmpclause);
        */
      array_insert_last(int, tmpclause, right);
        /*
        tmpclause  = array_alloc(int, 2);
        array_insert(int, tmpclause, 0, -right);
        array_insert(int, tmpclause, 1, cnfIndex);
        array_insert_last(array_t *, clauseArray, tmpclause);
        */
      BmcCnfInsertClause(cnfClauses, tmpclause);
      array_free(tmpclause);
      
      return cnfIndex;
    case Ctlsp_F_c:
      if (l >= 0){ /* loop */
        i = (l < i)? l: i;
      }
      cnfIndex = cnfClauses->cnfGlobalIndex++;
      clause   = array_alloc(int, 0);
      for (j=i; j<= k; j++){
        left      = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
        leftValue = checkIndex(left, cnfClauses);
        if (leftValue != -1){
          array_free(clause);
          return 0;
        }
        array_insert_last(int, clause, left);
          /*
          tmpclause  = array_alloc(int, 2);
          array_insert(int, tmpclause, 1, cnfIndex);
          array_insert(int, tmpclause, 0, -left);
          array_insert_last(array_t *, clauseArray, tmpclause);
          */
      }
      array_insert_last(int, clause, -cnfIndex);
      BmcCnfInsertClause(cnfClauses, clause);
      array_free(clause);
 
      return cnfIndex;
    case Ctlsp_G_c:
      if (l < 0){ /* FALSE */
        /* add an empty clause */
        BmcAddEmptyClause(cnfClauses);
        return 0;
      } else {
       i = (l < i)? l: i;
       andIndex = cnfClauses->cnfGlobalIndex++;
       for (j=i; j<= k; j++){
         left      = BmcGenerateCnfForLtl(network, ltlFormula->left, j, k, l, cnfClauses);
         leftValue = checkIndex(left, cnfClauses);
         if (leftValue != -1){
           return 0;
         }
         tmpclause  = array_alloc(int, 2);
         array_insert(int, tmpclause, 0, left);
         array_insert(int, tmpclause, 1, -andIndex);
         BmcCnfInsertClause(cnfClauses, tmpclause);
         array_free(tmpclause);
       }/* for j loop*/
      } /* else */
      return andIndex;
    case Ctlsp_X_c:
      /* X left */
      if((l >= 0) && (i == k) ){
        i = l;
      } else if (i < k){
        i = i + 1;
      } else { /* FALSE */
        /* add an empty clause */
        BmcAddEmptyClause(cnfClauses);
        return 0;
      }
      return BmcGenerateCnfForLtl(network, ltlFormula->left, i, k, l, cnfClauses);
    case Ctlsp_U_c: /* (left U right) */
      state = BmcCnfClausesFreeze(cnfClauses);
      
      leftValue  = 1; /* left is TRUE*/
      rightValue = 1; /* right is TRUE*/
      orIndex    = cnfClauses->cnfGlobalIndex++;
      orClause   = array_alloc(int, 0);
      array_insert_last(int, orClause, -orIndex);

      orValue = 0;
      for (j=i; j<= k; j++){
        right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
        rightValue = checkIndex(right, cnfClauses);
        andIndex   = cnfClauses->cnfGlobalIndex++;
        if (rightValue == -1){
          rightClause  = array_alloc(int, 2);
          array_insert(int, rightClause, 0, right);
          array_insert(int, rightClause, 1, -andIndex);
          BmcCnfInsertClause(cnfClauses, rightClause);
          array_free(rightClause);
        }
        andValue = rightValue;
        for (n=i; (n <= j-1) && (andValue != 0); n++){
          left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
          leftValue = checkIndex(left, cnfClauses);
          andValue  = doAnd(andValue, leftValue);
          if (leftValue == -1){
            leftClause  = array_alloc(int, 2);
            array_insert(int, leftClause, 0, left);
            array_insert(int, leftClause, 1, -andIndex);
            BmcCnfInsertClause(cnfClauses, leftClause);
            array_free(leftClause);
          }
        } /* for n loop */
        orValue = doOr(orValue, andValue);
        if (orValue == 1){ /* TRUE */
          break;
        }
        if (andValue != 0){
          array_insert_last(int, orClause, andIndex);
        }
      } /* for j loop*/
      if ( (l >=0) && (orValue !=1)){ /* loop */
        for (j=l; j<= i-1; j++){
          right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
          rightValue = checkIndex(right, cnfClauses);
          andIndex   = cnfClauses->cnfGlobalIndex++;
          if (rightValue == -1){
            rightClause  = array_alloc(int, 2);
            array_insert(int, rightClause, 0, right);
            array_insert(int, rightClause, 1, -andIndex);
            BmcCnfInsertClause(cnfClauses, rightClause);
            array_free(rightClause);
          }
          andValue = rightValue;  
          for (n=i; (n<= k) && (andValue != 0); n++){
            left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
            leftValue = checkIndex(left, cnfClauses);
            andValue  = doAnd(andValue, leftValue);
            if (leftValue == -1){
              leftClause  = array_alloc(int, 2);
              array_insert(int, leftClause, 0, left);
              array_insert(int, leftClause, 1, -andIndex);
              BmcCnfInsertClause(cnfClauses, leftClause);
              array_free(leftClause);
            }
          } /* for n loop */
          for (n=l; (n<= j-1)  && (andValue != 0); n++){
            left = BmcGenerateCnfForLtl(network, ltlFormula->left, n, k, l, cnfClauses);
            leftValue = checkIndex(left, cnfClauses);
            andValue  = doAnd(andValue, leftValue);
            if (leftValue == -1){
              leftClause  = array_alloc(int, 2);
              array_insert(int, leftClause, 0, left);
              array_insert(int, leftClause, 1, -andIndex);
              BmcCnfInsertClause(cnfClauses, leftClause);
              array_free(leftClause);
            }
          } /* for n loop */
          orValue = doOr(orValue, andValue);
          if (orValue == 1){ /* TRUE */
            break;
          }
          if (andValue != 0){
            array_insert_last(int, orClause, andIndex);
          }
        }/* j loop*/
      } /* if (l>=0) */
      if ((orValue == 1) || (orValue == 0)){
        /*restore the infomration back*/
        BmcCnfClausesRestore(cnfClauses, state);
        FREE(state);
        array_free(orClause);
        if (orValue == 0){
          /* add an empty clause*/
          BmcAddEmptyClause(cnfClauses);
        }
        return 0;
      } else {
        BmcCnfClausesUnFreeze(cnfClauses, state);
        FREE(state);
        BmcCnfInsertClause(cnfClauses, orClause);
        array_free(orClause);
        return orIndex;
      }
    case Ctlsp_R_c:
      /* (left R right) */
      state = BmcCnfClausesFreeze(cnfClauses);
      
      orIndex  = cnfClauses->cnfGlobalIndex++;
      orClause = array_alloc(int, 0);
      array_insert_last(int, orClause, -orIndex);
      
      orValue = 0;
      if (l >= 0){ /* loop */
        andIndex = cnfClauses->cnfGlobalIndex++;
        andValue = 1;
        for (j=(i<l?i:l); (j<= k) && (andValue != 0); j++){
          right = BmcGenerateCnfForLtl(network, ltlFormula->right, j, k, l, cnfClauses);
          rightValue = checkIndex(right, cnfClauses);
          andValue  = doAnd(andValue, rightValue);
          if (rightValue == -1){
            rightClause  = array_alloc(int, 2);
            array_insert(int, rightClause, 0, right);
            array_insert(int, rightClause, 1, -andIndex);
            BmcCnfInsertClause(cnfClauses, rightClause);
            array_free(rightClause);
          }
        } /* for j loop*/
        if (andValue == -1){
          array_insert_last(int, orClause, andIndex);
        }
        orValue = doOr(orValue, andValue);
      } /* loop */
      if(orValue != 1){
        for (j=i; j<= k; j++){
          left = BmcGenerateCnfForLtl(network, ltlFormula->left,
                                      j, k, l, cnfClauses);
          leftValue = checkIndex(left, cnfClauses);
          andIndex = cnfClauses->cnfGlobalIndex++;
          if (leftValue == -1){
            leftClause  = array_alloc(int, 2);
            array_insert(int, leftClause, 0, left);
            array_insert(int, leftClause, 1, -andIndex);
            BmcCnfInsertClause(cnfClauses, leftClause);
            array_free(leftClause);
          }
          andValue = leftValue;
          for (n=i; (n<= j) && (andValue != 0); n++){
            right = BmcGenerateCnfForLtl(network, ltlFormula->right,
                                         n, k, l, cnfClauses);
            rightValue = checkIndex(right, cnfClauses);
            andValue   = doAnd(andValue, rightValue);
            if (rightValue == -1){
              rightClause  = array_alloc(int, 2);
              array_insert(int, rightClause, 0, right);
              array_insert(int, rightClause, 1, -andIndex);
              BmcCnfInsertClause(cnfClauses, rightClause);
              array_free(rightClause);
            }
          } /* for n loop */
          orValue = doOr(orValue, andValue);
          if (orValue == 1){ /* TRUE */
            break;
          }
          if (andValue != 0){
            array_insert_last(int, orClause, andIndex);
          }
        }/* for j loop*/
        if ((l >= 0)  && (orValue !=1)) { /* loop */
          for (j=l; j<= i-1; j++){
            left = BmcGenerateCnfForLtl(network, ltlFormula->left,
                                        j, k, l, cnfClauses);
            leftValue = checkIndex(left, cnfClauses);
            andIndex = cnfClauses->cnfGlobalIndex++;
            if (leftValue == -1){
              leftClause  = array_alloc(int, 2);
              array_insert(int, leftClause, 0, left);
              array_insert(int, leftClause, 1, -andIndex);
              BmcCnfInsertClause(cnfClauses, leftClause);
              array_free(leftClause);
            }
            andValue = leftValue;
            for (n=i; (n<= k)  && (andValue != 0); n++){
              right = BmcGenerateCnfForLtl(network, ltlFormula->right,
                                           n, k, l, cnfClauses);
              rightValue = checkIndex(right, cnfClauses);
              andValue = doAnd(andValue, rightValue);
              if (rightValue == -1){
                rightClause  = array_alloc(int, 2);
                array_insert(int, rightClause, 0, right);
                array_insert(int, rightClause, 1, -andIndex);
                BmcCnfInsertClause(cnfClauses, rightClause);
                array_free(rightClause);
              }
            } /* for n loop */
            for (n=l; (n<= j) && (andValue != 0); n++){
              right = BmcGenerateCnfForLtl(network, ltlFormula->right,
                                           n, k, l, cnfClauses);
              rightValue = checkIndex(right, cnfClauses);
              andValue = doAnd(andValue, rightValue);
              if (rightValue == -1){
                rightClause  = array_alloc(int, 2);
                array_insert(int, rightClause, 0, right);
                array_insert(int, rightClause, 1, -andIndex);
                BmcCnfInsertClause(cnfClauses, rightClause);
                array_free(rightClause);
              }
            } /* for n loop */
            orValue = doOr(orValue, andValue);
            if (orValue == 1){ /* TRUE */
              break;
            }
            if (andValue != 0){
              array_insert_last(int, orClause, andIndex);
            }
          } /* for j loop*/
        } /* if (l>=0) */
      }/* orValue !=1*/
      if ((orValue == 1) || (orValue == 0)){
        /*restore the infomration back*/
        BmcCnfClausesRestore(cnfClauses, state);
        FREE(state);
        array_free(orClause);
        if (orValue == 0){
          /* add an empty clause*/
          BmcAddEmptyClause(cnfClauses);
        }
        return 0;
      } else {
        BmcCnfClausesUnFreeze(cnfClauses, state);
        FREE(state);
        BmcCnfInsertClause(cnfClauses, orClause);
        array_free(orClause);
        return orIndex;
      }
    default:
      fail("Unexpected LTL formula type");
      break;
  }
  return -1; /* we should never get here */
}
/*  BmcLTLFormulaNoLoopTranslation() */


void
BmcLtlCheckSafety(
   Ntk_Network_t   *network,
   Ctlsp_Formula_t *ltlFormula,
   BmcOption_t     *options,
   st_table        *CoiTable)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
  FILE              *cnfFile;
  int               noLoopIndex;
  array_t           *result = NIL(array_t);
  int               leftValue  = 0;
  long              startTime, endTime;
  int               k;
  int               minK = options->minK;
  int               maxK = options->maxK;
  boolean           boundedFormula;
  int               depth;
  array_t           *unitClause =  array_alloc(int, 1);
  
  array_t           *orClause =  array_alloc(int, 2);

  /* ************** */
  /* Initialization */
  /* ************** */
  startTime = util_cpu_ctime();
  /* 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));

  /* For bounded formulae use a tighter upper bound if possible. */
  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltlFormula, &depth);
  if (boundedFormula && depth < maxK && depth >= minK) {
    maxK = depth;
  }
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void) fprintf(vis_stdout, "saftey LTL BMC\n");
    if (boundedFormula){
      (void) fprintf(vis_stdout, "Bounded formula of depth %d\n", depth);
    }
    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  minK, maxK, options->step);
  }
  k= minK;
  while( (result == NIL(array_t)) && (k <= maxK)){
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }
    cnfClauses = BmcCnfClausesAlloc();
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return;
    }
    BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
                                 cnfClauses, nodeToMvfAigTable, CoiTable);
    noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
    leftValue   = checkIndex(noLoopIndex, cnfClauses);

    if(leftValue == 1){
      assert(k==1);
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,"# BMC: formula failed\n");
        (void) fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
      }
      break;
    } else if(leftValue == 0){
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,"# BMC: the formula is trivially true");
        (void) fprintf(vis_stdout," for counterexamples of length %d\n", k);
      }
      /*
      break;
      */
    } else {
      array_insert(int, unitClause, 0, noLoopIndex);
      
      BmcCnfInsertClause(cnfClauses, unitClause);
      
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      (void) fclose(cnfFile);
      result = BmcCheckSAT(options);
      if (options->satSolverError){
        break;
      }
      if(result != NIL(array_t)) {
        (void) fprintf(vis_stdout, "# BMC: formula failed\n");
        if(options->verbosityLevel != BmcVerbosityNone_c){
          (void) fprintf(vis_stdout,
                         "# BMC: Found a counterexample of length = %d \n", k);
        }
        if (options->dbgLevel == 1) {
          BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                                 result, k, CoiTable, options, NIL(array_t));
        }
        break;
      }
    }
    /* free all used memories */
    BmcCnfClausesFree(cnfClauses);
#if 0

    /*
      Check induction
     */
    {
      BmcCnfClauses_t   *noLoopCnfClauses = BmcCnfClausesAlloc();
      array_t           *noLoopResult = NIL(array_t);
      array_t           *unitClause =  array_alloc(int, 1);
      int               i;

      printf("Check Induction \n");

      cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
      if (cnfFile == NIL(FILE)) {
        (void)fprintf(vis_stderr,
                      "** bmc error: Cannot create CNF output file %s\n",
                      options->satInFile);
        return;
      }
      /*
        Generate a loop free path
      */
      BmcCnfGenerateClausesForLoopFreePath(network, 0, k+1, BMC_NO_INITIAL_STATES,
                                           noLoopCnfClauses, nodeToMvfAigTable, CoiTable);
      /*
        The property true at states from 0 to k
       */
      unitClause = array_alloc(int, 1);
      for(i=0; i<=k; i++){
        array_insert(int, unitClause, 0, 
                     -BmcGenerateCnfForLtl(network, ltlFormula, i, k, -1, noLoopCnfClauses));
        BmcCnfInsertClause(noLoopCnfClauses, unitClause);
      }
      
      /*
        The property fails at k +1
       */
      array_insert(int, unitClause, 0, 
                   BmcGenerateCnfForLtl(network, ltlFormula, 0, k+1, -1, noLoopCnfClauses));
      BmcCnfInsertClause(noLoopCnfClauses, unitClause);
      array_free(unitClause);
   
      BmcWriteClauses(manager, cnfFile, noLoopCnfClauses, options);
      (void) fclose(cnfFile);
      noLoopResult = BmcCheckSAT(options);
      if(noLoopResult == NIL(array_t)) {
        (void) fprintf(vis_stdout, "# BMC: formula passed\n");
        (void) fprintf(vis_stdout,
                       "# BMC: No more loop free path \n");
        
        break;
      }
      /*
        BmcPrintCounterExample(network, nodeToMvfAigTable, noLoopCnfClauses,
        noLoopResult, bound+1, CoiTable, options, NIL(array_t));
      */
      BmcCnfClausesFree(noLoopCnfClauses);
    } /* Check induction */
 
#endif
    k += options->step;

#if 0
    
    /* Check if reach the depth of the model */
    cnfClauses = BmcCnfClausesAlloc();
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return;
    }
    /*
      Generate a loop free path
     */
    {
      BmcCnfGenerateClausesForPath(network, 0, k, BMC_INITIAL_STATES,
                                   cnfClauses, nodeToMvfAigTable, CoiTable);
      /*
        initIndex   = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
        noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
        
        array_insert(int, orClause, 0, initIndex);
        array_insert(int, orClause, 1, -noLoopIndex);
        
        BmcCnfInsertClause(cnfClauses, orClause);
      */
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      (void) fclose(cnfFile);
      result = BmcCheckSAT(options);
      if(result == NIL(array_t)) {
        (void) fprintf(vis_stdout, "# BMC: formula passed\n");
        (void) fprintf(vis_stdout,
                       "# BMC: No more loop free path \n");
        
        return;
      }
      /*
        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
        result, k, CoiTable, options, NIL(array_t));
      */
      result = NIL(array_t);
    }
    BmcCnfClausesFree(cnfClauses);


    /* Check if reach the depth of the model */
    cnfClauses = BmcCnfClausesAlloc();
    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
    if (cnfFile == NIL(FILE)) {
      (void)fprintf(vis_stderr,
                    "** bmc error: Cannot create CNF output file %s\n",
                    options->satInFile);
      return;
    }
    /*
      Generate a loop free path
     */
    {
      BmcCnfGenerateClausesForPath(network, 0, k, BMC_NO_INITIAL_STATES,
                                   cnfClauses, nodeToMvfAigTable, CoiTable);
      /*
        initIndex   = BmcCnfGenerateClausesFromStateToState(network, -1, 0, cnfClauses, nodeToMvfAigTable, CoiTable, -1);
      */
      noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, -1, cnfClauses);
      array_insert(int, unitClause, 0, noLoopIndex);
      
      BmcCnfInsertClause(cnfClauses, unitClause);
      /*
        array_insert(int, orClause, 0, initIndex);
        array_insert(int, orClause, 1, -noLoopIndex);
        
        BmcCnfInsertClause(cnfClauses, orClause);
      */
      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
      (void) fclose(cnfFile);
      result = BmcCheckSAT(options);
      if(result == NIL(array_t)) {
        (void) fprintf(vis_stdout, "# BMC: (Bad state) formula passed\n");
        (void) fprintf(vis_stdout,
                       "# BMC: No more loop free path \n");
        
        return;
      }
      /*
        BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
        result, k, CoiTable, options, NIL(array_t));
      */
      result = NIL(array_t);
    }
    BmcCnfClausesFree(cnfClauses);
#endif
    
    
  } /* while result and k*/
  if (options->satSolverError == FALSE){
    if ((result == NIL(array_t)) && (k > maxK)){
      if (boundedFormula && depth <= options->maxK){
        (void) fprintf(vis_stdout,"# BMC: formula passed\n");
      } else {
        (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
      }
      if (options->verbosityLevel != BmcVerbosityNone_c){
        (void) fprintf(vis_stdout,
                       "# BMC: no counterexample found of length up to %d \n",
                       maxK);
      }
    }
  }
  /* free all used memories */
  if (k == 0){
     BmcCnfClausesFree(cnfClauses);
  }
  if(result != NIL(array_t)){
    array_free(result);
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  array_free(unitClause);
  array_free(orClause);
  fflush(vis_stdout);
  return;
} /* BmcLtlCheckSafety() */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


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
doAnd(
  int left,
  int right)
{
  if ((left == -1) && (right == -1)){
    return -1;
  }
  return (left * right);
  
} /* doAnd */

static int
doOr(
  int left,
  int right)
{
  if ((left == -1) || (right == -1)){
    return -1;
  }
  if ((left == 1) || (right == 1)){
    return 1;
  }
  return 0;
  
} /* doOr */