src/bmc/bmcCirCUs.c

Go to the documentation of this file.

#include "bmcInt.h"
#include "sat.h"
#include "baig.h"

static char rcsid[] UNUSED = "$Id: bmcCirCUs.c,v 1.56 2010/04/09 23:50:57 fabio Exp $";

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

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

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

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

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

static int printSatValue(bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue);
static int printSatValueAiger(bAig_Manager_t *manager, st_table *nodeToMvfAigTable, st_table *li2index, bAigEdge_t **baigArr, array_t *nodeArr, int bound, int *prevValue);
static int StringCheckIsInteger(char *string, int *value);
static int verifyIfConstant(bAigEdge_t property);

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

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

void
BmcCirCUsLtlVerifyProp(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    st_table        *coiTable,
    BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  bAigEdge_t        property;
  int               satFlag;
  satInterface_t    *interface;
  array_t           *objArray;

  assert(Ctlsp_isPropositionalFormula(ltl));

  startTime = util_cpu_ctime();
  if (options->verbosityLevel >= BmcVerbosityNone_c){
    fprintf(vis_stdout, "LTL formula is propositional\n");
  }
  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl);
  if (property == mAig_NULL){
    return;
  }
  if (verifyIfConstant(property)){
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }
 
  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
                                                           MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));
  
  interface = 0;
  objArray  = array_alloc(bAigEdge_t, 0);
  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
  property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
                                              0, ltl, BMC_INITIAL_STATES);
  array_insert(bAigEdge_t, objArray, 0, property);
  options->cnfPrefix = 0;
  interface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                           objArray, NIL(array_t),
                                           options, interface);
  satFlag = interface->status;
  sat_FreeInterface(interface);

  if(satFlag == SAT_SAT) {
    fprintf(vis_stdout, "# BMC: formula failed\n");
    if(options->dbgLevel == 1){
      fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, 0, 0,
                                   options, BMC_INITIAL_STATES);
    }
    if(options->dbgLevel == 2){
      fprintf(vis_stdout, "# BMC: found a counterexample of length 0\n");
      fprintf(vis_stdout, "# The counterexample for Structural Sat problem is incomplete.\n");
      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, 0, 0,
                                   options, BMC_INITIAL_STATES);
    }

  }
  else if(satFlag != SAT_SAT) {
    if(options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout,"# BMC: no counterexample found of length 0\n");
    }
    fprintf(vis_stdout,"# BMC: formula passed\n");
    (void) fprintf(vis_stdout, "#      Termination depth = 0\n");
  }
  if (options->verbosityLevel != BmcVerbosityNone_c){
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
  }
  array_free(objArray);
  fflush(vis_stdout);
  return;
} /* BmcCirCUsLtlVerifyProp() */


int
BmcCirCUsLtlCheckInductiveInvariant(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltl,
  BmcOption_t     *options,
  st_table        *CoiTable)
{
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  bAigEdge_t      property, result;
  int             satFlag;
  satInterface_t  *interface;
  array_t         *objArray   = array_alloc(bAigEdge_t, 1);
  int             returnValue = 0;  /* the property is not an inductive
                                       invariant */
  /*
    Check if the property holds in all initial states.
   */
  interface = 0;
  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
  property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_INITIAL_STATES);

  array_insert(bAigEdge_t, objArray, 0, property);
  options->cnfPrefix = 0;
  interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
                                 NIL(array_t), options, interface);
  satFlag = interface->status;
  sat_FreeInterface(interface);

  if(satFlag == SAT_UNSAT) {
    /*
      Check the induction step.
    */
    interface = 0;
    bAig_ExpandTimeFrame(network, manager, 2, BMC_NO_INITIAL_STATES);
    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 0, ltl->right, BMC_NO_INITIAL_STATES);
    /*
      The property is true at state 0.  Remember that the passing property is
      the negation of the original property.
    */
    result = bAig_Not(property);
    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, 1, ltl->right, BMC_NO_INITIAL_STATES);
    /*
      The property is false at state 1
    */
    result = bAig_And(manager, result, property);
    array_insert(bAigEdge_t, objArray, 0, result);
    options->cnfPrefix = 1;
    interface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
                                   NIL(array_t), options, interface);
    satFlag = interface->status;
    sat_FreeInterface(interface);
    if(satFlag == SAT_UNSAT) {
      returnValue = 1; /* the property is an inductive invariant */
     
    }
  }
  array_free(objArray);
  return returnValue; 
} /* BmcCirCUsLtlCheckInductiveInvariant */


void
BmcCirCUsLtlVerifyGp(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    st_table        *coiTable,
    BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  bAigEdge_t        property, result, simplePath;
  int               j, satFlag, k;
  int               checkInductiveInvariant;
  array_t           *objArray;
  array_t           *auxObjArray;
  satInterface_t    *ceInterface, *etInterface, *tInterface;
  st_table          *coiIndexTable;
  Bmc_PropertyStatus formulaStatus;

  assert(Ctlsp_LtlFormulaIsFp(ltl));
  
  startTime = util_cpu_ctime();

  if (options->verbosityLevel != BmcVerbosityNone_c){
    fprintf(vis_stdout, "LTL formula is of type G(p)\n");
  }
  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
  
  if (property == mAig_NULL){
    return;
  }
  if (verifyIfConstant(property)){
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }

  if (options->verbosityLevel >= BmcVerbosityMax_c){
    (void) fprintf(vis_stdout, "\nBMC: Check if the property is an inductive invariant\n");
  }
  checkInductiveInvariant = BmcCirCUsLtlCheckInductiveInvariant(network, ltl, options, coiTable);
  if (checkInductiveInvariant == 1){
    (void) fprintf(vis_stdout,"# BMC: The property is an inductive invariant\n");
    (void) fprintf(vis_stdout,"# BMC: formula passed\n");
    (void) fprintf(vis_stdout, "#      Termination depth = 0\n");
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }
  
  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
                                                           MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));

  ceInterface = 0;
  etInterface = 0;
  tInterface  = 0;
  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);
  }
  /*
    Hold objects 
  */
  objArray = array_alloc(bAigEdge_t, 2);
  /*
    Unused entry is set to bAig_One
   */
  array_insert(bAigEdge_t, objArray, 1, bAig_One);
  /*
    Hold auxiliary objects (constraints on the path)
  */
  auxObjArray = array_alloc(bAigEdge_t, 0);
  
  bAig_ExpandTimeFrame(network, manager, 1, BMC_NO_INITIAL_STATES); 
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
  
  formulaStatus = BmcPropertyUndecided_c;
  for(k = options->minK; k <= options->maxK; k += options->step){
    if (options->verbosityLevel == BmcVerbosityMax_c){
      fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", k);
    }
    /*
      Expand counterexample length to k.  In BMC, counterexample of length k means
      k+1 time frames.
     */
    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
    /*
      The property true at any states from (k-step+1) to k 
     */
    result = bAig_Zero;
    for(j=k-options->step+1; j<=k; j++) {
      /*
        For k = options->minK, j goes outside the lower boundary of
        counterexample search.
      */
      if(j < options->minK) continue;
      
      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, ltl->right, BMC_INITIAL_STATES);
      result   = bAig_Or(manager, result, property);
    }
    array_insert(bAigEdge_t, objArray, 0, result);
    options->cnfPrefix = k;
    ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network, objArray,
                                           auxObjArray, options,
                                           ceInterface);
    satFlag = ceInterface->status;
    if(satFlag == SAT_SAT){
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    /*
      Given that the property does not hold at all previous states.
     */
    array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));

    /*
      Prove if the property passes using the induction proof of SSS0.
    */
    if((options->inductiveStep !=0) &&
       (k % options->inductiveStep == 0)){
      array_t *auxArray;
      int i;
      
      if (options->verbosityLevel == BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
      }      
      /*
        Expand counterexample length to k+1.  In BMC, counterexample of length k+1 means
        k+2 time frames.
      */
      bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
      simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
                                                coiIndexTable, BMC_NO_INITIAL_STATES);
      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k+1, ltl->right,
                                                  BMC_NO_INITIAL_STATES);
      array_insert(bAigEdge_t, objArray, 0, simplePath);
      array_insert(bAigEdge_t, objArray, 1, property);
      auxArray = array_alloc(bAigEdge_t, 0);
      for(i=0; i<=k; i++){
        array_insert_last(bAigEdge_t, auxArray,
                          bAig_Not(
                            BmcCirCUsCreatebAigOfPropFormula(network, manager, i, ltl->right,
                                                             BMC_NO_INITIAL_STATES)
                            ));
      }
      options->cnfPrefix = k+1;
      tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                      objArray, auxArray,
                                      options, tInterface);
      array_free(auxArray); 
      array_insert(bAigEdge_t, objArray, 1, bAig_One);
      if(tInterface->status == SAT_UNSAT){
        if (options->verbosityLevel == BmcVerbosityMax_c) {
          (void) fprintf(vis_stdout,
                         "# BMC: No simple path leading to a bad state\n");
        }
        formulaStatus = BmcPropertyPassed_c;
        break;
      }
      
      if(options->earlyTermination){
        /*
          Early termination condition
          
          Check if there is no simple path starts from initial states
          
        */
        simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
                                                  coiIndexTable,
                                                  BMC_INITIAL_STATES);
        array_insert(bAigEdge_t, objArray, 0, simplePath);
        etInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                               objArray, NIL(array_t),
                                               options, etInterface);
        options->cnfPrefix = k+1;
        if(etInterface->status == SAT_UNSAT){
          if (options->verbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout,
                           "# BMC: No simple path starting at an initial state\n");
          }
          formulaStatus = BmcPropertyPassed_c;
          break;
        }
      }
      
    } /* check for termination*/
  } /* loop over k*/
  array_free(objArray);
  array_free(auxObjArray);
  sat_FreeInterface(ceInterface);
  if(etInterface !=0){
    sat_FreeInterface(etInterface);
  }
  if(tInterface !=0){
    sat_FreeInterface(tInterface);
  }
  st_free_table(coiIndexTable);

  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", k);
    }
    if(options->dbgLevel == 1){
      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, 0,
                                   options, BMC_INITIAL_STATES);
    }
    if(options->dbgLevel == 2){
      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, 0,
                                   options, BMC_INITIAL_STATES);
    }
  } else if(formulaStatus == BmcPropertyPassed_c) {
    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", k);
  } else if(formulaStatus == BmcPropertyUndecided_c) {
    (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
  }
  
  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;
} /* BmcCirCUsLtlVerifyGp() */

void
BmcCirCUsLtlVerifyFp(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    st_table        *coiTable,
    BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  bAigEdge_t        property, pathProperty, simplePath, tloop, loop;
  int               bound, k, satFlag;
  array_t           *loop_array = NIL(array_t);
  array_t           *objArray;
  array_t           *auxObjArray;
  st_table          *coiIndexTable;
  satInterface_t    *ceInterface;
  satInterface_t    *tInterface;
  Bmc_PropertyStatus formulaStatus;

  startTime = util_cpu_ctime();
  if(options->verbosityLevel != BmcVerbosityNone_c){
    fprintf(vis_stdout,"LTL formula is of type F(p)\n");
  }
  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
                                                      ltl->right);
  if (verifyIfConstant(property)){
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    return;
  }

  nodeToMvfAigTable = 
          (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));
  
  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);

 /*
    Hold objects 
  */
  objArray = array_alloc(bAigEdge_t, 2);
  /*
    Unused entry is set to bAig_One
   */
  array_insert(bAigEdge_t, objArray, 1, bAig_One);
  /*
    Hold auxiliary objects (constraints on the path)
  */
  auxObjArray = array_alloc(bAigEdge_t, 0);
  
  ceInterface = 0;
  tInterface  = 0;
  formulaStatus = BmcPropertyUndecided_c;
  if(options->verbosityLevel != BmcVerbosityNone_c){
    fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
                       options->minK, options->maxK, options->step);

  }
  bound = options->minK;
  while(bound<=options->maxK) {
    if(options->verbosityLevel == BmcVerbosityMax_c)
      fprintf(vis_stdout, "\nBMC: Generate counterexample of length %d\n", bound);
    /*
      Expand counterexample length to bound.  In BMC, counterexample of length bound means
      bound+1 time frames.
    */
    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES );
    loop_array = array_alloc(bAigEdge_t *, 0);
    tloop = bAig_Zero;
    /*
      Loop from state 'bound' to any previous states.
     */
    for(k=0; k<=bound; k++) {
      loop = BmcCirCUsConnectFromStateToState(network, bound, k, nodeToMvfAigTable,
                                              coiIndexTable, BMC_INITIAL_STATES);
      array_insert(bAigEdge_t, loop_array, k, loop);
      tloop = bAig_Or(manager, tloop, loop);
    }
    array_insert(bAigEdge_t, objArray, 0, tloop);
    /*
      tloop equals true for k-loop path 
     */
    /*
      Property false at all states
     */
    pathProperty = bAig_One;
    for(k=bound; k>=0; k--) {
      property = BmcCirCUsCreatebAigOfPropFormula(network, manager, k, ltl->right, BMC_INITIAL_STATES);
      pathProperty = bAig_And(manager, pathProperty, property);
    }
    array_insert(bAigEdge_t, objArray, 1, pathProperty);
    
    options->cnfPrefix = bound;
    ceInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                               objArray, auxObjArray,
                                               options, ceInterface);
    satFlag = ceInterface->status;
    if(satFlag == SAT_SAT){
      formulaStatus = BmcPropertyFailed_c;
      break;
    }

    array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(tloop));

    if((options->inductiveStep !=0) &&
       (bound % options->inductiveStep == 0)){

      if (options->verbosityLevel == BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout,
                       "\nBMC: Check for termination\n");
      }
      simplePath = BmcCirCUsSimlePathConstraint(network, 0, bound, nodeToMvfAigTable,
                                                coiIndexTable,
                                                BMC_INITIAL_STATES);
      array_insert(bAigEdge_t, objArray, 0, simplePath);
      array_insert(bAigEdge_t, objArray, 1, pathProperty);
      tInterface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                                objArray, auxObjArray,
                                                options, tInterface);
      if(tInterface->status == SAT_UNSAT){
        formulaStatus = BmcPropertyPassed_c;
        break;
      }
    }
    bound += options->step;
  }
  array_free(objArray);
  array_free(auxObjArray);
  st_free_table(coiIndexTable);
  sat_FreeInterface(ceInterface);
  sat_FreeInterface(tInterface);

  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);
    }
    if(options->dbgLevel == 1){
     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_array,
                                   options, BMC_INITIAL_STATES);
    }
    if(options->dbgLevel == 2){
     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_array,
                                   options, BMC_INITIAL_STATES);
    }

  } else if(formulaStatus == BmcPropertyPassed_c) {
    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", bound);
  } else if(formulaStatus == BmcPropertyUndecided_c) {
    (void) fprintf(vis_stdout,"# BMC: formula undecided\n");
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
  }
  fflush(vis_stdout);  
  array_free(loop_array);

} /* BmcCirCUsLtlVerifyFp() */

bAigEdge_t
BmcCirCUsGenerateLogicForLtl(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    int from,
    int to,
    int loop)
{
  bAigEdge_t property, temp;
  bAigEdge_t left, right, result;
  int j, k;
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);

  if(Ctlsp_isPropositionalFormula(ltl)){
    property = BmcCirCUsCreatebAigOfPropFormula(network, manager, from, ltl, BMC_INITIAL_STATES);
    return(property);
  }

  switch(ltl->type) {
    case Ctlsp_NOT_c:
      if (!Ctlsp_isPropositionalFormula(ltl->left)){
        fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");
        return 0;
      }
    case Ctlsp_AND_c:
      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
      if(left == bAig_Zero)     return(bAig_Zero);
      right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
      return(bAig_And(manager, left, right));
    case Ctlsp_OR_c:
      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
      if(left == bAig_One)      return(bAig_One);
      right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, from, to, loop);
      return(bAig_Or(manager, left, right));
    case Ctlsp_F_c:
      if(loop >= 0)     from = (loop<from) ? loop : from;
      result = bAig_Zero;
      for(j=from; j<=to; j++)  {
        left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
        if(left == bAig_One)    return(left);
        result = bAig_Or(manager, left, result);
      }
      return(result);
    case Ctlsp_G_c:
      if(loop < 0)      return(bAig_Zero);
      from = (loop < from) ? loop : from;
      result = bAig_One;
      for(j=from; j<=to; j++) {
        left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
        result = bAig_And(manager, result, left);
        if(result == bAig_Zero) break;
      }
      return(result);
    case Ctlsp_X_c:
      if(loop>=0 && from == to) from = loop;
      else if(from < to)        from = from + 1;
      else                      return(bAig_Zero);
      left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, from, to, loop);
      return(left);
    case Ctlsp_U_c:
      result = bAig_Zero;
      for(j=from; j<=to; j++) {
        right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
        temp = right;
        for(k=from; (k<=j-1); k++) {
          left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
          temp = bAig_And(manager, temp, left);
          if(temp == bAig_Zero) break;
        }
        result = bAig_Or(manager, result, temp);
        if(result == bAig_One) break;
      }
      if(loop>=0 && result != bAig_One) {
        for(j=loop; j<=from-1; j++) {
          right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
          temp = right;
          for(k=from; k<=to; k++) {
            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
            temp = bAig_And(manager, temp, left);
            if(temp == bAig_Zero)       break;
          }
          for(k=loop; k<=j-1; k++) {
            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, k, to, loop);
            temp = bAig_And(manager, temp, left);
            if(temp == bAig_Zero)       break;
          }
          result = bAig_Or(manager, result, temp);
          if(result == bAig_One) break;
        }
      }
      return(result);
    case Ctlsp_R_c:
      result = bAig_Zero;
      if(loop >= 0) {
        temp = bAig_One;
        for(j=(from<loop ? from : loop); j<=to; j++) {
          right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, j, to, loop);
          temp = bAig_And(manager, temp, right);
          if(temp == bAig_Zero) break;
        }
        result = bAig_Or(manager, result, temp);
      }
      if(result != bAig_One) {
        for(j=from; j<=to; j++) {
          left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);
          temp = left;
          for(k=from; k<=j; k++) {
            right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
            temp = bAig_And(manager, temp, right);
            if(temp == bAig_Zero)       break;
          }
          result = bAig_Or(manager, temp, result);
          if(result == bAig_One) break;
        }
        if(loop >= 0 && result != bAig_One) {
          for(j=loop; j<=from-1; j++) {
            left = BmcCirCUsGenerateLogicForLtl(network, ltl->left, j, to, loop);

            temp = left;
            for(k=from; k<=to; k++) {
              right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
              temp = bAig_And(manager, temp, right);
              if(temp == bAig_Zero)     break;
            }

            for(k=loop; k<=j; k++) {
              right = BmcCirCUsGenerateLogicForLtl(network, ltl->right, k, to, loop);
              temp = bAig_And(manager, temp, right);
              if(temp == bAig_Zero)     break;
            }

            result = bAig_Or(manager, result, temp);
            if(result == bAig_One) break;
          }
        }
      }
      return(result);
    default:
      fail("Unexpected LTL formula type");
      break;
  }
  assert(0);
  return(-1);

}

bAigEdge_t
BmcCirCUsGenerateLogicForLtlSNF(
  Ntk_Network_t   *network,
  array_t         *formulaArray,
  int             fromState,
  int             toState,
  int             loop)
{
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  Ctlsp_Formula_t *formula;
  bAigEdge_t      property = bAig_One;
  bAigEdge_t      left, right, result;
  int             i, k;
  Ctlsp_Formula_t *leftChild, *rightChild;

  for (i = 0; i < array_n(formulaArray); i++) { 
    formula    = array_fetch(Ctlsp_Formula_t *, formulaArray, i);  
    leftChild  = Ctlsp_FormulaReadLeftChild(formula);
    rightChild = Ctlsp_FormulaReadRightChild(formula);

    if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFstart")){
      result = BmcCirCUsGenerateLogicForLtl(network, rightChild,
                                            0, toState, loop);
    } else 
      if(!strcmp(Ctlsp_FormulaReadVariableName(leftChild), " SNFbound")){
        result =  BmcCirCUsGenerateLogicForLtl(network, rightChild,
                                               toState, toState, loop);
      } else {
        result = bAig_One;
        for(k=fromState; k<= toState; k++){
          left  = BmcCirCUsGenerateLogicForLtl(network, leftChild,
                                               k, toState, loop);
          right = BmcCirCUsGenerateLogicForLtl(network, rightChild,
                                               k, toState, loop);
          result = bAig_And(manager, result,
                            bAig_Then(manager, left, right));
        }
      }
    property = bAig_And(manager, property, result);
  }
  return property;
} /* BmcCirCUsGenerateLogicForLtlSNF */


bAigEdge_t
BmcCirCUsGenerateLogicForLtlFixPoint(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltl,
  int             from,
  int             to,
  array_t         *loopArray)
{
  bAigEdge_t result;
  st_table   *ltl2AigTable;

  assert(ltl != NIL(Ctlsp_Formula_t));
  
  ltl2AigTable = st_init_table(strcmp, st_strhash);
  result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
                                  from, to, 0, loopArray, ltl2AigTable);
  st_free_table(ltl2AigTable);

  return result;
} /* BmcCirCUsGenerateLogicForLtlFixPoint */

bAigEdge_t
BmcCirCUsGenerateLogicForLtlFixPointRecursive(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltl,
  int             from,
  int             to,
  int             translation, /* 0 auxilary translation. 1 final translation */
  array_t         *loopArray,
  st_table        *ltl2AigTable)
{
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  bAigEdge_t      property, temp;
  bAigEdge_t      left, right, result;

  int      j;

  char     *nameKey;
  char     tmpName[100];

  /*
    Check if AIG was built for this LTL formula at a given time
   */
  sprintf(tmpName, "%ld_%d%d", (long)ltl, from, translation);
  nameKey = util_strsav(tmpName);
  if(st_lookup(ltl2AigTable, nameKey, &result)){
    FREE(nameKey);
    return result;
  }
  FREE(nameKey);
  
  if(Ctlsp_isPropositionalFormula(ltl)){
    property = BmcCirCUsCreatebAigOfPropFormula(network, manager,
                                                from, ltl, BMC_INITIAL_STATES);
    sprintf(tmpName, "%ld_%d%d", (long)ltl, from, 1);
    nameKey = util_strsav(tmpName);
    st_insert(ltl2AigTable, nameKey, (char*) (long) property);
    return(property);
  }
  switch(ltl->type) {
  case Ctlsp_NOT_c:
    if (!Ctlsp_isPropositionalFormula(ltl->left)){
      fprintf(vis_stderr,"BMC error: the LTL formula is not in NNF\n");

      return 0;
    }
  case Ctlsp_AND_c:
    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
                                                         translation, loopArray, ltl2AigTable);
    if(left == bAig_Zero){
      return(bAig_Zero);
    }
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
                                                          translation, loopArray, ltl2AigTable);
    return(bAig_And(manager, left, right));
  case Ctlsp_OR_c:
    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from, to,
                                                         translation, loopArray, ltl2AigTable);
    if(left == bAig_One){
      return(bAig_One);
    }
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, from, to,
                                                          translation, loopArray, ltl2AigTable);
    return(bAig_Or(manager, left, right));
  case Ctlsp_X_c:
    if(from < to){
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left, from+1, to,
                                                             1, loopArray, ltl2AigTable);
    } else {
      result =  bAig_Zero;
      for(j=1; j<=to; j++) {
        left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to,
                                                              1, loopArray, ltl2AigTable);
        temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j), left);
        result = bAig_Or(manager, result, temp);
      }
    }
    sprintf(tmpName, "%ld_%d%d", (long) ltl, from, 1);
    nameKey = util_strsav(tmpName);
    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    return result;
  case Ctlsp_U_c:
    sprintf(tmpName, "%ld_%d%d", (long) ltl, to, 0); /* 0 for auxiliary translation*/
    nameKey = util_strsav(tmpName);
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
    st_insert(ltl2AigTable, nameKey, (char*) (long) right);
    /*
      Compute the auxiliary translation.
    */
    for(j=to-1; j>=from; j--) {
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
      
      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
      
      result  = bAig_And(manager,left, result);
      result  = bAig_Or(manager,right, result);
      
      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
      nameKey = util_strsav(tmpName);
      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    }
    /*
      Compute the final translation at k.
    */
    result =  bAig_Zero;
    for(j=1; j<=to; j++) {
      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
      result = bAig_Or(manager, result, temp);
    }
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
    left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
                                                          to, to, 1, loopArray,
                                                          ltl2AigTable);
    
    result  = bAig_And(manager,left, result);
    result  = bAig_Or(manager,right, result);
    
    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 1); /* 1 for final translation*/
    nameKey = util_strsav(tmpName);
    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    /*
      Compute the final translation.
    */
    for(j=to-1; j>=from; j--) {
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);

      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
    
      result  = bAig_And(manager,left, result);
      result  = bAig_Or(manager,right, result);

      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
      nameKey = util_strsav(tmpName);
      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    }
    return(result);
  case Ctlsp_R_c:
    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, to, to, 1, loopArray, ltl2AigTable);
    nameKey = util_strsav(tmpName);
    st_insert(ltl2AigTable, nameKey, (char*) (long) right);
    /*
      Compute the auxiliary translation.
    */
    for(j=to-1; j>=from; j--) {
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 0, loopArray, ltl2AigTable);
      
      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
      
      result  = bAig_Or(manager,left, result);
      result  = bAig_And(manager,right, result);
      
      sprintf(tmpName, "%ld_%d%d", (long) ltl, j, 0); /* 0 for auxiliary translation*/
      nameKey = util_strsav(tmpName);
      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    }
    /*
      Compute the final translation at k.
    */
    result =  bAig_Zero;
    for(j=1; j<=to; j++) {
      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
      result = bAig_Or(manager, result, temp);
    }
    right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right,
                                                          to, to, 1, loopArray,
                                                          ltl2AigTable);
    left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
                                                          to, to, 1, loopArray,
                                                          ltl2AigTable);    
    result  = bAig_Or(manager,left, result);
    result  = bAig_And(manager,right, result);
    
    sprintf(tmpName, "%ld_%d%d", (long) ltl, to+1, 1); /* 1 for final translation*/
    nameKey = util_strsav(tmpName);
    st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    /*
      Compute the final translation.
    */
    for(j=to-1; j>=from; j--) {
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl, j+1, to, 1, loopArray, ltl2AigTable);

      right = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->right, j, to, 1, loopArray, ltl2AigTable);
      left  = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,  j, to, 1, loopArray, ltl2AigTable);
    
      result  = bAig_Or(manager,left, result);
      result  = bAig_And(manager,right, result);

      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 1);
      nameKey = util_strsav(tmpName);
      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    }
    return(result);
  case Ctlsp_F_c:
    /*
      Compute only the auxiliary translation.
    */
    sprintf(tmpName, "%ld_%d%d", (long)ltl, to, 0); /* 0 for auxiliary translation*/
    nameKey = util_strsav(tmpName);
    left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
                                                         to, to, 1, loopArray,
                                                         ltl2AigTable);
    st_insert(ltl2AigTable, nameKey, (char*) (long) left);

    for(j=to-1; j>=from; j--) {
      result = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl,
                                                             j+1, to, 0,
                                                             loopArray,
                                                             ltl2AigTable);
      left = BmcCirCUsGenerateLogicForLtlFixPointRecursive(network, ltl->left,
                                                           j, to, 1, loopArray,
                                                           ltl2AigTable);
      result  = bAig_Or(manager,left, result);
      
      sprintf(tmpName, "%ld_%d%d", (long)ltl, j, 0); /* 0 for auxiliary translation*/
      nameKey = util_strsav(tmpName);
      st_insert(ltl2AigTable, nameKey, (char*) (long) result);
    }
    result =  bAig_Zero;
    for(j=1; j<=to; j++) {
      temp = bAig_And(manager, array_fetch(bAigEdge_t, loopArray, j),
                      BmcCirCUsGenerateLogicForLtlFixPointRecursive(
                        network, ltl, j, to, 0, loopArray, ltl2AigTable));
      result = bAig_Or(manager, result, temp);
    }
    return(result);
  default:
    fail("Unexpected LTL formula type");
    break;
  }
  assert(0);
  return(-1);
}

void
BmcCirCUsLtlVerifyFGp(
   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 */

  int              j, k, l, satFlag;

  long             startTime, endTime;
  int              minK = options->minK;
  int              maxK = options->maxK;
  Ctlsp_Formula_t  *propFormula;
  bAigEdge_t       property, loop, pathProperty, tloop;
  array_t          *loop_array = NIL(array_t);
  array_t          *previousResultArray;
  st_table         *coiIndexTable;
  satInterface_t   *ceInterface;
  
  Bmc_PropertyStatus formulaStatus;

  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 */
  /* ************** */
  
  startTime = util_cpu_ctime();
  if(options->verbosityLevel >= BmcVerbosityMax_c){
    fprintf(vis_stdout,"LTL formula is of type FG(p)\n");
  }
  propFormula = Ctlsp_FormulaReadRightChild(Ctlsp_FormulaReadRightChild(ltlFormula));
  property = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager,
                                                      propFormula);
  if (verifyIfConstant(property)){
    if (options->verbosityLevel != BmcVerbosityNone_c){
      fprintf(vis_stdout, "-- bmc time = %10g\n",
              (double)(util_cpu_ctime() - startTime) / 1000.0);
    }
    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));
  
  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
  
  previousResultArray = array_alloc(bAigEdge_t, 0);
  ceInterface = 0;
  if(options->verbosityLevel != BmcVerbosityNone_c){
    fprintf(vis_stdout,"Apply BMC on counterexample of length >= %d and <= %d (+%d)\n",
            options->minK, options->maxK, options->step);
    
  }
  k= minK;
  formulaStatus = BmcPropertyUndecided_c;
  while(k <= maxK){
    if (options->verbosityLevel >= BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }
   /*
     Expand counterexample length to bound.  In BMC, counterexample of length bound means
     k+1 time frames.
   */
    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES );

    /*
      k-loop
    */
    loop_array = array_alloc(bAigEdge_t *, 0);
    tloop = bAig_Zero;
    /*
      Loop from last state to any previous states.
    */
    for(l=0; l<=k; l++) {
      loop = BmcCirCUsConnectFromStateToState(network, k, l, nodeToMvfAigTable,
                                              coiIndexTable, BMC_INITIAL_STATES);
      array_insert(bAigEdge_t, loop_array, l, loop);
      pathProperty = bAig_Zero;
      for(j=l; j<=k; j++){
        property = BmcCirCUsCreatebAigOfPropFormula(network, manager, j, propFormula, BMC_INITIAL_STATES);
        pathProperty = bAig_Or(manager, pathProperty, property);
      }
      
      tloop = bAig_Or(manager, tloop, bAig_And(manager, pathProperty, loop));
    }
    options->cnfPrefix = k;
    ceInterface = BmcCirCUsInterface(manager, network, tloop,
                                     previousResultArray, options,
                                     ceInterface);
    satFlag = ceInterface->status;
    if(satFlag == SAT_SAT){
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    array_free(loop_array);

    /* ==================
       Prove termination
       ================== */
    if((checkLevel < 3) &&
       (options->inductiveStep !=0) &&
       (k % options->inductiveStep == 0))
      {
        satInterface_t *tInterface=0, *etInterface=0;
        bAigEdge_t     simplePath, property;
        int            i;
        
        /* ===========================
           Early termination condition
           ===========================
        */
        if (options->earlyTermination) {
          if (options->verbosityLevel >= BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "\nChecking for early termination at k= %d\n", k);
          }
          bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
                                                    coiIndexTable, BMC_INITIAL_STATES);
          options->cnfPrefix = k;
          etInterface = BmcCirCUsInterface(manager, network,
                                           simplePath,
                                           previousResultArray,
                                           options, etInterface);
          if(etInterface->status == SAT_UNSAT){
            formulaStatus = BmcPropertyPassed_c;
            if (options->verbosityLevel >= BmcVerbosityMax_c) {
              (void) fprintf(vis_stdout, "# BMC: by early termination\n");
            }
            break;
          }
        } /* Early termination */
        /*
          Check for \beta''(k)
        */
        if(checkLevel == 0){
          if (options->verbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
          }
          
          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
          property = bAig_One;
          for(i=1; i<=k+1; i++){
            property = bAig_And(manager, property,
                                bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
                                  network, manager, i,
                                  propFormula, BMC_NO_INITIAL_STATES)));
          }
          property = bAig_And(manager, property,
                              BmcCirCUsCreatebAigOfPropFormula(
                                network, manager, 0,
                                propFormula, BMC_NO_INITIAL_STATES));
          options->cnfPrefix = k+1;
          tInterface = 0;
          tInterface = BmcCirCUsInterface(manager, network,
                                          bAig_And(manager, property, simplePath),
                                          previousResultArray, options, tInterface);
          if(tInterface->status == SAT_UNSAT){
            m = k;
            if (options->verbosityLevel >= BmcVerbosityMax_c) {
              (void)fprintf(vis_stderr,"m = %d\n", m);
            }
            checkLevel = 1;
          }
        } /* Check for Beta'' */
        /*
          Check for \beta'(k)
        */
        if(checkLevel == 0){
          if (options->verbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
          }
          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
          property = bAig_One;
          for(i=0; i<=k; i++){
            property = bAig_And(manager, property,
                                bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
                                  network, manager, i,
                                  propFormula, BMC_NO_INITIAL_STATES)));
          }
          property = bAig_And(manager, property,
                              BmcCirCUsCreatebAigOfPropFormula(
                                network, manager, k+1,
                                propFormula, BMC_NO_INITIAL_STATES));
          options->cnfPrefix = k+1;
          tInterface = 0;
          tInterface = BmcCirCUsInterface(manager, network,
                                          bAig_And(manager, property, simplePath),
                                          previousResultArray, options, tInterface);
          if(tInterface->status == SAT_UNSAT){
            m = k;
            if (options->verbosityLevel >= BmcVerbosityMax_c) {
              (void)fprintf(vis_stderr,"m = %d\n", m);
            }
            checkLevel = 1;
          } 
        } /* Check for Beta' */
        /*
          Check for Beta
        */
        if(checkLevel == 1){
          if (options->verbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
          }
          bAig_ExpandTimeFrame(network, manager, k+2, BMC_NO_INITIAL_STATES);
          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k+1, nodeToMvfAigTable,
                                                 coiIndexTable, BMC_NO_INITIAL_STATES);
          property = bAig_And(manager,
                              bAig_Not(BmcCirCUsCreatebAigOfPropFormula(
                                network, manager, k,
                                propFormula, BMC_NO_INITIAL_STATES)),
                              BmcCirCUsCreatebAigOfPropFormula(
                                network, manager, k+1,
                                propFormula, BMC_NO_INITIAL_STATES));
          options->cnfPrefix = k+1;
          tInterface = BmcCirCUsInterface(manager, network,
                                          bAig_And(manager, property, simplePath),
                                          previousResultArray, options, tInterface);
          if(tInterface->status == SAT_UNSAT){
            checkLevel = 2;
          }
        } /* Check Beta*/
  
        if(checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
          if (options->verbosityLevel == BmcVerbosityMax_c) {
            (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
          }
          bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);
          simplePath = BmcCirCUsSimlePathConstraint(network, 0, k, nodeToMvfAigTable,
                                                  coiIndexTable, BMC_INITIAL_STATES);
          property = BmcCirCUsCreatebAigOfPropFormula(
                                  network, manager, k,
                                  propFormula, BMC_INITIAL_STATES);
          options->cnfPrefix = k;
          tInterface = 0;
          tInterface = BmcCirCUsInterface(manager, network,
                                          bAig_And(manager, property, simplePath),
                                          previousResultArray, options, tInterface);
          if(tInterface->status == SAT_UNSAT){
            n = k;
            checkLevel = 3;
            if (options->verbosityLevel == BmcVerbosityMax_c) {
              (void)fprintf(vis_stdout,"Value of m=%d  n=%d\n", m, n);
            }
            if (m+n-1 <= maxK){
              maxK = m+n-1;
              checkLevel = 3;
            } else {
              checkLevel = 4;
            }
          }
        }/* Chek for Alpha */
        
        if (options->verbosityLevel != BmcVerbosityNone_c) {
          endTime = util_cpu_ctime();
          fprintf(vis_stdout, "-- Check for termination time = %10g\n",
                  (double)(endTime - startTime) / 1000.0);
        }
  
      } /* Check for termination */
    k += options->step;
  } /* while result and k*/
 
  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){
      BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, k, loop_array,
                                   options, BMC_INITIAL_STATES);
    }
    if(options->dbgLevel == 2){
      BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, k, loop_array,
                                   options, BMC_INITIAL_STATES);
    }

    array_free(loop_array);
  }
  if(checkLevel == 3){
    (void) fprintf(vis_stdout, "# BMC: no counterexample of length <= (m+n-1) %d is found \n", m+n-1);
    formulaStatus = BmcPropertyPassed_c;
  }
  if(formulaStatus == BmcPropertyPassed_c) {
    (void) fprintf(vis_stdout, "# BMC: formula Passed\n");
    (void) fprintf(vis_stdout, "#      Termination depth = %d\n", k);
  } 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);
  }
  
  array_free(previousResultArray);
  
  fflush(vis_stdout);
  return;
} /* BmcCirCUsLtlVerifyGFp() */

void
BmcCirCUsLtlVerifyGeneralLtl(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    st_table        *coiTable,
    array_t         *constraintArray,
    BmcOption_t     *options,
    int             snf)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  boolean           fairness  = (options->fairFile != NIL(FILE));
  int               minK = options->minK;
  int               maxK = options->maxK;
  boolean           boundedFormula;
  array_t           *ltlConstraintArray = NIL(array_t);
  array_t           *fairnessArray = NIL(array_t);
  int               depth, l, bound, f, satFlag, i;
  bAigEdge_t        noLoop, loop, ploop; 
  bAigEdge_t        result=bAig_NULL, temp, fair;
  array_t           *loop_arr = NIL(array_t);
  array_t           *objArray;
  array_t           *auxObjArray;
  st_table          *coiIndexTable;
  Ctlsp_Formula_t   *formula;
  satInterface_t    *interface;
  array_t           *formulaArray = NIL(array_t);
  int               nextAction = 0;
  /*
    Use when proving termination
   */
  BmcCheckForTermination_t *terminationStatus = 0;
  Bmc_PropertyStatus       formulaStatus;

  nodeToMvfAigTable = 
          (st_table *) Ntk_NetworkReadApplInfo(network,
                                               MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));

  if(fairness) {
    Ctlsp_Formula_t *formula; /* a generic LTL formula */
    int              i;       /* iteration variable */

    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);
    
    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
      fprintf(vis_stdout, "Formula: ddd");
      Ctlsp_FormulaPrint(vis_stdout, formula);
      fprintf(vis_stdout, "\n");
      BmcGetCoiForLtlFormula(network, formula, coiTable);
      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
      array_insert_last(Ctlsp_Formula_t *, ltlConstraintArray, formula);
    }
  }
  /*
    For bounded formulae use a tighter upper bound if possible.
  */
  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &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(ltl),
                                                 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);
  }
  bAig_ExpandTimeFrame(network, manager, 1, 1);
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
  interface    = 0;
  /*
    Hold objects 
  */
  objArray = array_alloc(bAigEdge_t, 1);
  /*
    Hold auxiliary objects (constraints on the path)
  */
  auxObjArray = array_alloc(bAigEdge_t, 0);

  formulaStatus = BmcPropertyUndecided_c;
  bound = minK;
  if(snf){
    formulaArray = Ctlsp_LtlTranslateIntoSNF(ltl);
  }
  startTime = util_cpu_ctime();
  while(bound<=maxK) {
    if(options->verbosityLevel == BmcVerbosityMax_c){
      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
    }

    loop_arr = 0;
    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);

    if(fairness){
      /*
        In case of fairness constraints, we only include a loop part of BMC
        encoding
      */
      noLoop = bAig_Zero;
    } else {
      if(snf){
        noLoop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0, bound, -1);
      } else {
        noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
      }
    }
    result = noLoop;
    if(noLoop != bAig_One) {
      loop_arr = array_alloc(bAigEdge_t, 0);
      for(l=0; l<=bound; l++) {
        if(snf){
          loop = BmcCirCUsGenerateLogicForLtlSNF(network, formulaArray, 0,
                                                 bound, l);
        } else { 
          loop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, l);
        }
        if(loop == bAig_Zero)   continue;

        if(fairness) {
          fairnessArray = array_alloc(bAigEdge_t, 0);
          arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
            fair = BmcCirCUsGenerateLogicForLtl(network, formula, l, bound, -1);
            array_insert_last(bAigEdge_t, fairnessArray, fair);
          }
        }

        if(loop != bAig_Zero) {
          ploop = BmcCirCUsConnectFromStateToState(network, bound, l, nodeToMvfAigTable, coiIndexTable, 1);
          array_insert(bAigEdge_t, loop_arr, l, ploop);
          temp = bAig_And(manager, loop, ploop);
          if(fairness) {
            for(f=0; f < array_n(fairnessArray); f++){
              fair = array_fetch(bAigEdge_t, fairnessArray, f);
              temp = bAig_And(manager, temp, fair); 
            }
          }
          result = bAig_Or(manager, result, temp);
        }
        if(fairness){
          array_free(fairnessArray);
        }
      }
    }
    /*
    loop = result;
    
    if((noLoop == bAig_Zero) && (loop == bAig_Zero)){
    */
    /*
      result = noLoop | loop(0) | loop(1) ... | loop(bound)
     */
    
    if(result == bAig_Zero){
      if (options->verbosityLevel != BmcVerbosityNone_c){
        fprintf(vis_stdout,"# BMC: the formula is trivially true");
        fprintf(vis_stdout," for counterexamples of length %d\n", bound);
      }
    } else {
      array_insert(bAigEdge_t, objArray, 0, result);
      options->cnfPrefix = bound;
      interface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                               objArray, auxObjArray,
                                               options, interface);
      satFlag = interface->status;
      if(satFlag == SAT_SAT) {
        formulaStatus = BmcPropertyFailed_c;
        break;
      }
      array_insert_last(bAigEdge_t, auxObjArray, bAig_Not(result));
    }
    /*
      Use the termination check if the the LTL formula is not bounded
    */
    if(!boundedFormula &&
       (formulaStatus == BmcPropertyUndecided_c) &&
       (nextAction != 1)){
      if((options->inductiveStep !=0) &&
         (bound % options->inductiveStep == 0))
        {
          /*
            Check for termination for the current value of k.
          */
          terminationStatus->k = bound;
          BmcCirCUsAutLtlCheckForTermination(network, manager,
                                             nodeToMvfAigTable,
                                             terminationStatus,
                                             coiIndexTable, options);
          nextAction = terminationStatus->action;
          if(nextAction == 1){
            maxK = terminationStatus->k;
          } else
            if(nextAction == 3){
              formulaStatus = BmcPropertyPassed_c;
              break;
            }
        }
    } /* terminationStatus */
    
    if(loop_arr) {
      array_free(loop_arr);
    }
    bound += options->step;
  }
  array_free(objArray);
  array_free(auxObjArray);
  st_free_table(coiIndexTable);
  sat_FreeInterface(interface);

  if(formulaStatus == BmcPropertyUndecided_c){
    if(nextAction == 1){
      /*
        No counterexample of length up to maxK is found. By termination
        criterion, formula passes
      */
      formulaStatus = BmcPropertyPassed_c;
    } else 
      if (boundedFormula && depth <= options->maxK){
        /*
          No counterexample of length up to the bounded depth of the LTL formula is
          found. Formula passes
        */
        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", bound);
      }
      if (options->dbgLevel == 1) {
        BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
                                     options, BMC_INITIAL_STATES);
      }
      if (options->dbgLevel == 2) {
        BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, loop_arr,
                                     options, BMC_INITIAL_STATES);
      }
    } 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);
      }
    }
  }
 
  /*
    free all used memories
  */
  if(terminationStatus){
    BmcAutTerminationFree(terminationStatus);
  }
  if(fairness){
    array_free(ltlConstraintArray);
  }
  if(snf){
    Ctlsp_FormulaArrayFree(formulaArray);
  }
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
  }

  fflush(vis_stdout);
}

void
BmcCirCUsLtlVerifyGeneralLtlFixPoint(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    st_table        *coiTable,
    array_t         *constraintArray,
    BmcOption_t     *options)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  bAigEdge_t        property, fair;
  boolean           fairness  = (options->fairFile != NIL(FILE));
  int               minK = options->minK;
  int               maxK = options->maxK;
  boolean           boundedFormula;
  array_t           *ltlConstraintArray = NIL(array_t);
  array_t           *objArray;
  array_t           *auxObjArray;
  st_table          *coiIndexTable;
  Ctlsp_Formula_t   *formula;
  satInterface_t    *interface;
  int               nextAction = 0;
  
  BmcCheckForTermination_t *terminationStatus = 0;
  Bmc_PropertyStatus       formulaStatus;
 
  array_t    *loopArray = NIL(array_t), *smallerExists;
  bAigEdge_t tmp, loop, atMostOnce, loopConstraints;
  int        i, k, depth, satFlag;
  
  startTime = util_cpu_ctime();

  nodeToMvfAigTable = 
          (st_table *) Ntk_NetworkReadApplInfo(network,
                                               MVFAIG_NETWORK_APPL_KEY);
  assert(nodeToMvfAigTable != NIL(st_table));

  if(fairness) {    
    ltlConstraintArray = array_alloc(Ctlsp_Formula_t *, 0);

    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
      BmcGetCoiForLtlFormula(network, formula, coiTable);
      formula =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
      array_insert(Ctlsp_Formula_t *, ltlConstraintArray, i, formula);
    }
  }

  /*
    For bounded formulae use a tighter upper bound if possible.
  */
  boundedFormula = Ctlsp_LtlFormulaTestIsBounded(ltl, &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(ltl),
                                                 constraintArray);
      assert(terminationStatus);
    }
  }
  
  if (options->verbosityLevel != BmcVerbosityNone_c){
    (void) fprintf(vis_stdout, "General LTL BMC\n");
    (void) fprintf(vis_stdout, "Apply BMC on counterexample of length >= %d and <= %d (+%d) \n",
                  minK, maxK, options->step);
  }

  bAig_ExpandTimeFrame(network, manager, 1, BMC_INITIAL_STATES);
  /*
    We need the above line inorder to run the next one.
   */
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
  interface = 0;

  /*
    Hold objects 
  */
  objArray = array_alloc(bAigEdge_t, 3);
  /*
    Hold auxiliary objects (constraints on the path)
  */
  auxObjArray = array_alloc(bAigEdge_t, 0);

  formulaStatus = BmcPropertyUndecided_c;
  k = minK;
  while(k<=maxK) {
    if(options->verbosityLevel == BmcVerbosityMax_c){
      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", k);
    }
    bAig_ExpandTimeFrame(network, manager, k+1, BMC_INITIAL_STATES);

    loopArray = array_alloc(bAigEdge_t, k+1);
    array_insert(bAigEdge_t, loopArray, 0, bAig_Zero);
    smallerExists   = array_alloc(bAigEdge_t, k+1);
    array_insert(bAigEdge_t, smallerExists, 0, bAig_Zero);

    loop = bAig_One;
    for(i=1; i<= k; i++){
      tmp = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
      array_insert(bAigEdge_t, loopArray, i, tmp);
      tmp = bAig_Then(manager, tmp,
                      BmcCirCUsConnectFromStateToState(network, k-1, i-1, nodeToMvfAigTable,
                                                       coiIndexTable, BMC_INITIAL_STATES));
      loop = bAig_And(manager, loop, tmp); 
    }
    array_insert(bAigEdge_t, smallerExists, 1, bAig_Zero);
    for(i=1; i<= k; i++){
      bAigEdge_t left, right;

      left = array_fetch(bAigEdge_t, smallerExists, i);
      right = array_fetch(bAigEdge_t, loopArray, i);
      
      array_insert(bAigEdge_t, smallerExists, i+1,
                   bAig_Or(manager, left, right));
    }
    atMostOnce =  bAig_One;
    for(i=1; i<= k; i++){
      bAigEdge_t left, right;

      left = array_fetch(bAigEdge_t, smallerExists, i);
      right = array_fetch(bAigEdge_t, loopArray, i);
      
      tmp = bAig_Then(manager, left, bAig_Not(right));
      atMostOnce = bAig_And(manager, atMostOnce, tmp);
    }

    loopConstraints = bAig_And(manager, loop, atMostOnce);

    property = BmcCirCUsGenerateLogicForLtlFixPoint(network, ltl, 0, k, loopArray);

    if(fairness) {
      fair = bAig_One;
      arrayForEachItem(Ctlsp_Formula_t *, ltlConstraintArray, i, formula) {
        fair = bAig_And(manager, fair,
                        BmcCirCUsGenerateLogicForLtlFixPoint(network, formula,
                                                             0, k, loopArray));
      }
      array_insert(bAigEdge_t, objArray, 2, fair);
    } else {
      array_insert(bAigEdge_t, objArray, 2,  bAig_One);
    }

    array_insert(bAigEdge_t, objArray, 0, loopConstraints);
    array_insert(bAigEdge_t, objArray, 1, property);
    options->cnfPrefix = k;
    interface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                             objArray, objArray,
                                             options, interface);
    array_free(smallerExists);
    
    satFlag = interface->status;
    if(satFlag == SAT_SAT) {
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    array_free(loopArray);
    /*
      Use the termination check if the the LTL formula is not bounded
    */
    if(!boundedFormula &&
       (formulaStatus == BmcPropertyUndecided_c) &&
       (nextAction != 1)){
      if((options->inductiveStep !=0) &&
         (k % options->inductiveStep == 0))
        {
          /*
            Check for termination for the current value of k.
          */
          terminationStatus->k = k;
          BmcCirCUsAutLtlCheckForTermination(network, manager,
                                             nodeToMvfAigTable,
                                             terminationStatus,
                                             coiIndexTable, options);
          nextAction = terminationStatus->action;
          if(nextAction == 1){
            maxK = terminationStatus->k;
          } else 
            if(nextAction == 3){
              formulaStatus = BmcPropertyPassed_c;
              maxK = k;
              break;
            }

        }
    } /* terminationStatus */
      
    k += options->step;
  }
  array_free(objArray);
  array_free(auxObjArray);
  st_free_table(coiIndexTable);
  sat_FreeInterface(interface);

  if(formulaStatus == BmcPropertyUndecided_c){
    /*
      If no counterexample of length up to a certain bound, then the property
      passes.
    */
    if(nextAction == 1){
      formulaStatus = BmcPropertyPassed_c;
    } else 
      if (boundedFormula && depth <= options->maxK){
        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) {
        int loop = k;
        /*
          Adjust loopArray to print a proper counterexample.  The encoding
          scheme does not differentiate between loop and no-loop path.  If the
          path has a loop, then the path length is k-1.
        */
        for(i=1; i< k; i++){
          bAigEdge_t   v      = array_fetch(bAigEdge_t, loopArray, i+1);
          unsigned int lvalue = aig_value(v); 
          
          if(lvalue == 1) {
            loop = k-1;
          }
          array_insert(bAigEdge_t, loopArray, i, v);
        }
        if (options->dbgLevel == 1) {
          BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable,
                                     coiTable, loop, loopArray,
                                     options, BMC_INITIAL_STATES);
        }
        if (options->dbgLevel == 1) {
          BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable,
                                     coiTable, loop, loopArray,
                                     options, BMC_INITIAL_STATES);
        }
        array_free(loopArray);
      }
    } 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);
      }
    }
  }
  
  /*
    free all used memories
  */
  if(terminationStatus){
    BmcAutTerminationFree(terminationStatus);
  }
  if(fairness){
     array_free(ltlConstraintArray);
  }
 
  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- bmc time = %10g\n", (double)(endTime - startTime) / 1000.0);
  }

  fflush(vis_stdout);
}


void
BmcCirCUsLtlCheckSafety(
    Ntk_Network_t   *network,
    Ctlsp_Formula_t *ltl,
    BmcOption_t     *options,
    st_table        *coiTable)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table);
  long              startTime, endTime;
  bAigEdge_t        noLoop;
  int               depth, satFlag, bound;
  int               minK = options->minK;
  int               maxK = options->maxK;
  int               boundedFormula;
  array_t           *previousResultArray;
  satInterface_t    *interface;
  array_t           *objArray;
  BmcCheckForTermination_t *terminationStatus = 0;
  Bmc_PropertyStatus       formulaStatus;
  st_table          *coiIndexTable;

  assert(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(ltl));
  
  startTime = util_cpu_ctime();

  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(ltl, &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(ltl),
                                                 NIL(array_t));
      assert(Ltl_AutomatonGetStrength(terminationStatus->automaton) == 0); /* Terminal Automaton*/
      assert(terminationStatus);
    }
  }
  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);
  }
  satFlag   = SAT_UNSAT;
  bAig_ExpandTimeFrame(network, manager, 0, BMC_INITIAL_STATES);
  coiIndexTable = BmcCirCUsGetCoiIndexTable(network, coiTable);
  interface = 0;
  formulaStatus = BmcPropertyUndecided_c;
  /*
    Hold objects 
  */
  objArray = array_alloc(bAigEdge_t, 1);

  previousResultArray = array_alloc(bAigEdge_t, 0);
  bound=minK;
  while(bound<=maxK) {
    
    if(options->verbosityLevel == BmcVerbosityMax_c)
      fprintf(vis_stdout, "\nGenerate counterexample of length %d\n", bound);
    fflush(vis_stdout);

    bAig_ExpandTimeFrame(network, manager, bound+1, BMC_INITIAL_STATES);

    /*
      A counterexample to a safety property is finite path at which the
      safety property does not hold.
     */
    noLoop = BmcCirCUsGenerateLogicForLtl(network, ltl, 0, bound, -1);
    array_insert(bAigEdge_t, objArray, 0, noLoop);
    
    options->cnfPrefix = bound;
    interface = BmcCirCUsInterfaceWithObjArr(manager, network,
                                             objArray,
                                             previousResultArray,
                                             options,
                                             interface);
    satFlag = interface->status;
    if(satFlag == SAT_SAT) {
      formulaStatus = BmcPropertyFailed_c;
      break;
    }
    array_insert_last(bAigEdge_t, previousResultArray, bAig_Not(noLoop));

    /*
      Use the termination check if the the LTL formula is not bounded
    */
    if(!boundedFormula &&
       (options->inductiveStep !=0) &&
       (bound % options->inductiveStep == 0))
      {
        terminationStatus->k = bound;
        BmcCirCUsAutLtlCheckTerminalAutomaton(network, manager,
                                              nodeToMvfAigTable,
                                              terminationStatus,
                                              coiIndexTable, options);
        if(terminationStatus->action == 1){
          formulaStatus = BmcPropertyPassed_c;
          maxK = bound;
          break;
        }
      }
    bound += options->step;
  }
  array_free(objArray);
  array_free(previousResultArray);
  sat_FreeInterface(interface);

  if ((formulaStatus != BmcPropertyFailed_c) && boundedFormula && depth <= options->maxK){
    /*
      No counterexample of length up to the bounded depth of the LTL formula is
      found. Formula passes
    */
    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", bound);
      }
      if (options->dbgLevel == 1) {
        BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
                                     options, BMC_INITIAL_STATES);
      }
      if (options->dbgLevel == 2) {
        BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, coiTable, bound, NIL(array_t),
                                     options, BMC_INITIAL_STATES);
      }
    } 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);
  }
  fflush(vis_stdout);  
  return;

}


bAigEdge_t
BmcCirCUsConnectFromStateToState(
    Ntk_Network_t   *network,
    int from,
    int to,
    st_table *nodeToMvfAigTable,
    st_table *coiIndexTable,
    int withInitialState)
{
  bAigEdge_t *fli, *tli;
  bAigEdge_t loop, tv;
  int l, index, nLatches;
  bAigTimeFrame_t *timeframe;
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);

  if(withInitialState)  timeframe = manager->timeframe;
  else                  timeframe = manager->timeframeWOI;

  fli = timeframe->latchInputs[from+1];
  tli = timeframe->latchInputs[to]; 
  loop = bAig_One;
  nLatches = timeframe->nLatches;
  for(l=0; l<nLatches; l++) {
    if(!st_lookup_int(coiIndexTable, (char *)(long)l, &index))  continue;
    tv = bAig_Eq(manager, fli[l], tli[l]);
    loop = bAig_And(manager, tv, loop);
    if(loop == bAig_Zero)       break;
  }
  return(loop);
}


bAigEdge_t
BmcCirCUsSimlePathConstraint(
  Ntk_Network_t *network,
  int           fromState,
  int           toState,
  st_table      *nodeToMvfAigTable,
  st_table      *coiIndexTable,
  int withInitialState)
{
  int             i, j; 
  bAigEdge_t      loop, nLoop;
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);

  nLoop = bAig_One;
  for(i=fromState+1; i<=toState; i++) {
    for(j=fromState; j<i; j++) {
      /*
        We want state Si == Sj, but the following function returns
        S(i+1) == Sj.  So we call the function with i-1.
      */
      loop = BmcCirCUsConnectFromStateToState(
             network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
      nLoop = bAig_And(manager, nLoop, bAig_Not(loop));
    }
  }
  return(nLoop);
} /* BmcCirCUsSimplePathConstraint */


bAigEdge_t
BmcCirCUsGenerateSimplePath(
        Ntk_Network_t   *network,
        int from,
        int to,
        st_table *nodeToMvfAigTable,
        st_table *coiIndexTable,
        int withInitialState)
{
int i, j; 
bAigEdge_t loop, nloop;
mAig_Manager_t    *manager;
    
  manager = Ntk_NetworkReadMAigManager(network);

  bAig_ExpandTimeFrame(network, manager, to, withInitialState);

  nloop = bAig_One;
  for(i=from+1; i<=to; i++) {
    for(j=from; j<i; j++) {
      loop = BmcCirCUsConnectFromStateToState(
             network, i-1, j, nodeToMvfAigTable, coiIndexTable, withInitialState);
      nloop = bAig_And(manager, nloop, bAig_Not(loop));
    }
  }
  return(nloop);
}


void
BmcCirCUsPrintCounterExample(
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  st_table        *coiTable,
  int             length,
  array_t         *loop_arr,
  BmcOption_t     *options,
  int withInitialState)
{
  int *prevLatchValues, *prevInputValues;
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  int loop, k;
  unsigned int lvalue;
  bAigEdge_t v;
  array_t *latchArr;
  lsGen gen;
  Ntk_Node_t *node;
  int tmp;
  bAigTimeFrame_t *timeframe;
  FILE *dbgOut = NULL;

  latchArr = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachLatch(network, gen, node){
    if (st_lookup_int(coiTable, (char *) node, &tmp)){
      array_insert_last(Ntk_Node_t *, latchArr, node);
    }
  }

  if(options->dbgOut)
  {
    dbgOut = vis_stdout;
    vis_stdout = options->dbgOut;
  }

  if(withInitialState)  timeframe = manager->timeframe;
  else                  timeframe = manager->timeframeWOI;

  prevLatchValues = ALLOC(int, timeframe->nLatches);
  prevInputValues = ALLOC(int, timeframe->nInputs);

  loop = -1;
  if(loop_arr != 0) {
    for(k=array_n(loop_arr)-1; k>=0; k--) {
      v = array_fetch(bAigEdge_t, loop_arr, k);
      lvalue = aig_value(v);
      if(lvalue == 1) {
        loop = k;
        break;
      }
    }
  }
  for(k=0; k<=length; k++) {
    if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
    else       fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
  
    printSatValue(manager, nodeToMvfAigTable, 
                    timeframe->li2index, 
                    timeframe->latchInputs, latchArr,
                    k, prevLatchValues);

    if(options->printInputs == TRUE && k!=0) {
      fprintf(vis_stdout, "--On input:\n");
      printSatValue(manager, nodeToMvfAigTable, 
                    timeframe->pi2index,
                    timeframe->inputs, timeframe->inputArr,
                    k-1, prevInputValues);
    }
  }

  if(loop >=0) {
    fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);

    printSatValue(manager, nodeToMvfAigTable, 
                    timeframe->li2index,
                    timeframe->latchInputs, latchArr,
                    loop, prevLatchValues);

    if(options->printInputs == TRUE && k!=0) {
      fprintf(vis_stdout, "--On input:\n");
      printSatValue(manager, nodeToMvfAigTable, 
                    timeframe->pi2index,
                    timeframe->inputs, timeframe->inputArr,
                    length, prevInputValues);
    }
  }

  array_free(latchArr);
  if(options->dbgOut)
  {
    vis_stdout = dbgOut;
  }
  return;
}



void
BmcCirCUsPrintCounterExampleAiger(
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  st_table        *coiTable,
  int             length,
  array_t         *loop_arr,
  BmcOption_t     *options,
  int withInitialState)
{
  int *prevLatchValues, *prevInputValues;
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  int loop, k;
  unsigned int lvalue;
  bAigEdge_t v;
  array_t *latchArr;
  lsGen gen;
  Ntk_Node_t *node;
  int tmp;
  bAigTimeFrame_t *timeframe;
  FILE *dbgOut = NULL;

  latchArr = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachLatch(network, gen, node){
    if (st_lookup_int(coiTable, (char *) node, &tmp)){
      array_insert_last(Ntk_Node_t *, latchArr, node);
    }
  }

  /* writing into a file is not being done in a standard way, need to confirm
     the writing of trace into a file with the vis standard */

  if(options->dbgOut)
  {
    dbgOut = vis_stdout;
    vis_stdout = options->dbgOut;
  }

  if(withInitialState)  timeframe = manager->timeframe;
  else                  timeframe = manager->timeframeWOI;

  prevLatchValues = ALLOC(int, timeframe->nLatches);
  prevInputValues = ALLOC(int, timeframe->nInputs);

  loop = -1;
  if(loop_arr != 0) {
    for(k=array_n(loop_arr)-1; k>=0; k--) {
      v = array_fetch(bAigEdge_t, loop_arr, k);
      lvalue = aig_value(v);
      if(lvalue == 1) {
        loop = k;
        break;
      }
    }
  }
  
  /* we need to get rid of the file generation for next vis release and look
     into ntk package so that the original order can be maintained */

  FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0) ;
  for(k=0; k<array_n(timeframe->inputArr); k++)
  {
    node = array_fetch(Ntk_Node_t *, timeframe->inputArr, k);
    fprintf(order, "%s\n", Ntk_NodeReadName(node));
  }
  fclose(order);
    
  for(k=0; k<=length; k++) {
    /*if(k == 0) fprintf(vis_stdout, "\n--State %d:\n", k);
    else       fprintf(vis_stdout, "\n--Goes to state %d:\n", k);*/

    /*if((loop>=0)||(k<length))
    { */
      printSatValueAiger(manager, nodeToMvfAigTable, 
                    timeframe->li2index, 
                    timeframe->latchInputs, latchArr,
                    k, prevLatchValues);
      fprintf(vis_stdout, " ");

    if((loop<0)||(k<length))
    { 
      if(k!=length+1) {
        printSatValueAiger(manager, nodeToMvfAigTable, 
                    timeframe->pi2index,
                    timeframe->inputs, timeframe->inputArr,
                    k, prevInputValues);
        fprintf(vis_stdout, " ");
      }

      if(k!=length+1) {
        printSatValueAiger(manager, nodeToMvfAigTable, 
                    timeframe->o2index,
                    timeframe->outputs, timeframe->outputArr,
                    k, prevInputValues);
        fprintf(vis_stdout, " ");
      }

      if(k!=length+1) {
        printSatValueAiger(manager, nodeToMvfAigTable,
                    timeframe->li2index,
                    timeframe->latchInputs, latchArr,
                    k+1, prevLatchValues);
        fprintf(vis_stdout, " ");
      }
      if((loop < 0)||(k!=length))
      {
        fprintf(vis_stdout, "\n");
      }
    }
  }

  if(loop >=0) {
    /*fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);*/

    if(k!=0) {
      printSatValueAiger(manager, nodeToMvfAigTable,
                    timeframe->pi2index,
                    timeframe->inputs, timeframe->inputArr,
                    length, prevInputValues);
      fprintf(vis_stdout, " ");
    }

    printSatValueAiger(manager, nodeToMvfAigTable,
                    timeframe->o2index,
                    timeframe->outputs, timeframe->outputArr,
                    k, prevInputValues);
    fprintf(vis_stdout, " ");

    printSatValueAiger(manager, nodeToMvfAigTable, 
                    timeframe->li2index,
                    timeframe->latchInputs, latchArr,
                    loop, prevLatchValues);
    
    fprintf(vis_stdout, "\n");
  }

  array_free(latchArr);
  if(options->dbgOut)
  {
    vis_stdout = dbgOut;
  }
  return;
} /* BmcCirCUsPrintCounterExampleAiger */

static int
printSatValue(
    bAig_Manager_t *manager,
    st_table        *nodeToMvfAigTable,
    st_table *li2index,
    bAigEdge_t **baigArr,
    array_t *nodeArr, 
    int bound,
    int *prevValue)
{
  Ntk_Node_t * node;
  int value, lvalue;
  char *symbolicValue;
  bAigEdge_t *li, v, tv;
  int i, j, timeframe, index;
  int changed=0;
  MvfAig_Function_t  *mvfAig;

  timeframe = bound;
  li = baigArr[timeframe];
  for(i=0; i<array_n(nodeArr); i++) {
    if(timeframe == 0)  prevValue[i] = -1;
    node = array_fetch(Ntk_Node_t *, nodeArr, i);
    mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);

    if(mvfAig == 0)     continue;

    value = -1;
    for (j=0; j< array_n(mvfAig); j++) {
      v = MvfAig_FunctionReadComponent(mvfAig, j);
      index = -1;
      if(!st_lookup_int(li2index, (char *)v, &index)) {
        fprintf(vis_stdout, "printSatValueERROR \n");
      }
      v = li[index];
      if(v == bAig_One) {
        value = j;
        break;
      }

      if(v != bAig_Zero) {
        tv = bAig_GetCanonical(manager, v);
        lvalue = bAig_GetValueOfNode(manager, tv);
        if(lvalue == 1){        
          value = j;
          break;
        }
      }
    }
    if(value >=0) {
      if (value != prevValue[i]){
        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
        prevValue[i] = value;
        changed = 1;
        if (Var_VariableTestIsSymbolic(nodeVar)) {
          symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
          fprintf(vis_stdout,"%s:%s\n",  Ntk_NodeReadName(node), symbolicValue);
        } 
        else {
          fprintf(vis_stdout,"%s:%d\n",  Ntk_NodeReadName(node), value);
        }
      }
    }
  } /* for j loop */
  if (changed == 0){
    fprintf(vis_stdout, "<Unchanged>\n");
  }
  return 0;
}

static int
printSatValueAiger(
    bAig_Manager_t *manager,
    st_table        *nodeToMvfAigTable,
    st_table *li2index,
    bAigEdge_t **baigArr,
    array_t *nodeArr, 
    int bound,
    int *prevValue)
{
  Ntk_Node_t * node;
  int value, lvalue;
  char *symbolicValue;
  bAigEdge_t *li, v, tv;
  int i, j, timeframe, index;
  MvfAig_Function_t  *mvfAig;

  timeframe = bound;
  li = baigArr[timeframe];
  for(i=0; i<array_n(nodeArr); i++) {
    if(timeframe == 0)  prevValue[i] = -1;
    node = array_fetch(Ntk_Node_t *, nodeArr, i);
    mvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);

    if(mvfAig == 0)     continue;

    value = -1;
    for (j=0; j< array_n(mvfAig); j++) {
      v = MvfAig_FunctionReadComponent(mvfAig, j);
      index = -1;
      if(!st_lookup_int(li2index, (char *)v, &index)) {
        fprintf(vis_stdout, "printSatValueERROR \n");
      }
      v = li[index];
      if(v == bAig_One) {
        value = j;
        break;
      }

      if(v != bAig_Zero) {
        tv = bAig_GetCanonical(manager, v);
        lvalue = bAig_GetValueOfNode(manager, tv);
        if(lvalue == 1){        
          value = j;
          break;
        }
      }
    }
    if(value >=0) {
      Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
      prevValue[i] = value;
      if (Var_VariableTestIsSymbolic(nodeVar)) {
        symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
        fprintf(vis_stdout,"%s", symbolicValue);
      } 
      else {
        fprintf(vis_stdout,"%d", value);
      }
    }
    else
    {
      fprintf(vis_stdout,"x");
    }
  } /* for j loop */
  return 0;
} /* printSatValueAiger */

bAigEdge_t 
BmcCirCUsCreatebAigOfPropFormula(
    Ntk_Network_t *network,
    bAig_Manager_t *manager,
    int bound,
    Ctlsp_Formula_t *ltl,
    int withInitialState)
{
  int index;
  bAigEdge_t result, left, right, *li;
  bAigTimeFrame_t *timeframe;

  if (ltl == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
  if (ltl->type == Ctlsp_TRUE_c)        return mAig_One; 
  if (ltl->type == Ctlsp_FALSE_c)       return mAig_Zero; 

  assert(Ctlsp_isPropositionalFormula(ltl));
  
  if(withInitialState) timeframe = manager->timeframe;
  else                 timeframe = manager->timeframeWOI;

  if (ltl->type == Ctlsp_ID_c){
      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);

      Var_Variable_t *nodeVar;
      int             nodeValue;

      MvfAig_Function_t  *tmpMvfAig;
      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
      
      if (node == NIL(Ntk_Node_t)) {
        char   *nameKey;
        char   tmpName[100];
        
        sprintf(tmpName, "%s_%d", nodeNameString, bound);
        nameKey = util_strsav(tmpName);

        result  = bAig_FindNodeByName(manager, nameKey);
        if(result == bAig_NULL){
           result = bAig_CreateVarNode(manager, nameKey); 
        } else {
          
          FREE(nameKey);
        }

        
        return result;
      }

      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
      assert(nodeToMvfAigTable != NIL(st_table));

      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
          array_free(tmpMvfAig);
          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      }
      
      nodeVar = Ntk_NodeReadVariable(node);
      if (Var_VariableTestIsSymbolic(nodeVar)) {
        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
        if ( nodeValue == -1 ) {
          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
        }
      }
      else { 
        int check;    
         check = StringCheckIsInteger(nodeValueString, &nodeValue);
         if( check == 0 ) {
          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if( check == 1 ) {
          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;

         }
      }
      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
      result = bAig_GetCanonical(manager, result);
      if(st_lookup_int(timeframe->li2index, (char *)result, &index)) {
        li = timeframe->latchInputs[bound];
        result = bAig_GetCanonical(manager, li[index]);
      }
      else if(st_lookup_int(timeframe->o2index, (char *)result, &index)) {
        li = timeframe->outputs[bound];
        result = bAig_GetCanonical(manager, li[index]);
      }
      else if(st_lookup_int(timeframe->i2index, (char *)result, &index)) {
        li = timeframe->internals[bound];
        result = bAig_GetCanonical(manager, li[index]);
      }
      return result;
  }

  left = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
  if (left == mAig_NULL){
    return mAig_NULL;
  }  
  right = BmcCirCUsCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
  if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
    return mAig_Not(left);
  }  
  else if(right == mAig_NULL) {
    return mAig_NULL;
  }

  switch(ltl->type) {
    case Ctlsp_OR_c:
      result = mAig_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = mAig_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = mAig_Then(manager, left, right); 
      break;
    case Ctlsp_EQ_c:
      result = mAig_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = mAig_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected type");
  }
  return result;
} /* BmcCirCUsCreatebAigOfPropFormula */

bAigEdge_t 
BmcCirCUsCreatebAigOfPropFormulaOriginal(
    Ntk_Network_t *network,
    bAig_Manager_t *manager,
    Ctlsp_Formula_t *ltl
    )
{
  bAigEdge_t result, left, right;

  if (ltl == NIL(Ctlsp_Formula_t))      return mAig_NULL; 
  if (ltl->type == Ctlsp_TRUE_c)        return mAig_One; 
  if (ltl->type == Ctlsp_FALSE_c)       return mAig_Zero; 

  assert(Ctlsp_isPropositionalFormula(ltl));
    
  if (ltl->type == Ctlsp_ID_c){
      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);

      Var_Variable_t *nodeVar;
      int             nodeValue;

      MvfAig_Function_t  *tmpMvfAig;
      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
      
      if (node == NIL(Ntk_Node_t)) {
          (void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
          return mAig_NULL;
      }

      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
      if (nodeToMvfAigTable == NIL(st_table)){
         (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
         return mAig_NULL;
      }
      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
          array_free(tmpMvfAig);
          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      }
      
      nodeVar = Ntk_NodeReadVariable(node);
      if (Var_VariableTestIsSymbolic(nodeVar)) {
        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
        if ( nodeValue == -1 ) {
          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
        }
      }
      else { 
        int check;    
         check = StringCheckIsInteger(nodeValueString, &nodeValue);
         if( check == 0 ) {
          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if( check == 1 ) {
          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;

         }
      }
      result = bAig_GetCanonical(manager,
              MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
      return result;
  }

  left = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->left);
  if (left == mAig_NULL){
    return mAig_NULL;
  }  
  right = BmcCirCUsCreatebAigOfPropFormulaOriginal(network, manager, ltl->right);
  if (right == mAig_NULL && ltl->type ==Ctlsp_NOT_c ){
    return mAig_Not(left);
  }  
  else if(right == mAig_NULL) {
    return mAig_NULL;
  }

  switch(ltl->type) {
    case Ctlsp_OR_c:
      result = mAig_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = mAig_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = mAig_Then(manager, left, right); 
      break;
    case Ctlsp_EQ_c:
      result = mAig_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = mAig_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected LTL type");
  }
  return result;
} /* BmcCirCUsCreatebAigOfPropFormulaOriginal */

static int
StringCheckIsInteger(
  char *string,
  int *value)
{
  char *ptr;
  long l;
  
  l = strtol (string, &ptr, 0) ;
  if(*ptr != '\0')
    return 0;
  if ((l > MAXINT) || (l < -1 - MAXINT))
    return 1 ;
  *value = (int) l;
  return 2 ;
}


satInterface_t *
BmcCirCUsInterface(
    bAig_Manager_t *manager,
    Ntk_Network_t  *network,
    bAigEdge_t     object,
    array_t        *auxObjectArray,
    BmcOption_t    *bmcOption,
    satInterface_t *interface)
{
satManager_t   *cm;
satOption_t    *option;
satLevel_t *d;
int i, size;
bAigEdge_t tv;

/* allocate sat manager */
  cm = sat_InitManager(interface);
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;
  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;
  if(interface)
    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(object == 0)      cm->status = SAT_UNSAT;
  else if(object == 1) cm->status = SAT_SAT;

  if(cm->status == 0) {
    cm->obj = sat_ArrayAlloc(1);
    sat_ArrayInsert(cm->obj, object);

    /* initialize option */
    option = sat_InitOption();
    option->cnfPrefix = bmcOption->cnfPrefix;
    /*option->verbose = bmcOption->verbosityLevel; */
    option->verbose = 0;
    option->timeoutLimit = bmcOption->timeOutPeriod;

    sat_SetIncrementalOption(option, bmcOption->incremental);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager, cm);
    /* value reset.. */
    sat_CleanDatabase(cm);
    /* set cone of influence */
    sat_SetConeOfInfluence(cm);
    sat_AllocLiteralsDB(cm);

    if(bmcOption->cnfFileName != NIL(char)) {
      sat_WriteCNF(cm, bmcOption->cnfFileName);
    }
    if(bmcOption->clauses == 0){ /* CirCUs circuit*/
      if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {      
        fprintf(vis_stdout,
                "Number of Variables = %d Number of Clauses = %d\n",
                sat_GetNumberOfInitialVariables(cm),  sat_GetNumberOfInitialClauses(cm));
      }
      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
        (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
        (void) fflush(vis_stdout);
      }
      sat_Main(cm);
      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout," done ");
        (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
      }
      
    } else if(bmcOption->clauses == 1) { /* CirCUs CNF */
      satArray_t *result;
      char       *fileName = NIL(char);
   
      sat_WriteCNF(cm, bmcOption->satInFile);
      if(bmcOption->satSolver == cusp){
        fileName = BmcCirCUsCallCusp(bmcOption);
      }
      if(bmcOption->satSolver == CirCUs){
        fileName = BmcCirCUsCallCirCUs(bmcOption);
      }
      if(fileName != NIL(char)){
        result = sat_ReadForcedAssignment(fileName);
        d =  sat_AllocLevel(cm);
        sat_PutAssignmentValueMain(cm, d, result);
        sat_ArrayFree(result);
      }
    }   
  }
  sat_CombineStatistics(cm);

  if(interface == 0)
    interface = ALLOC(satInterface_t, 1);

  interface->total = cm->total;
  interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
  interface->objUnitLitArray = 0;
  interface->savedConflictClauses = cm->savedConflictClauses;
  interface->trieArray = cm->trieArray;
  interface->status = cm->status;
  cm->total = 0;
  cm->nonobjUnitLitArray = 0;
  cm->savedConflictClauses = 0;

  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
    manager->maxNodesArraySize = cm->maxNodesArraySize;
    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
  }
  manager->NodesArray = cm->nodesArray;
  manager->literals = cm->literals;

  /* For the case that the input contains CNF clauese; */
  if(cm->literals)
    cm->literals->last = cm->literals->initialSize;
  cm->nodesArray = 0;
  cm->HashTable = 0;
  cm->timeframe = 0;
  cm->timeframeWOI = 0;
  cm->literals = 0;

  sat_FreeManager(cm);

  return(interface);
}

satInterface_t *
BmcCirCUsInterfaceWithObjArr(
    bAig_Manager_t *manager,
    Ntk_Network_t *network,
    array_t *objectArray,
    array_t *auxObjectArray,
    BmcOption_t *bmcOption,
    satInterface_t *interface)
{
satManager_t *cm;
satOption_t *option;
int i, size;
bAigEdge_t tv;

/* allocate sat manager */
  cm = sat_InitManager(interface);
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;
  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;
  if(interface)
    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(objectArray) {
    cm->obj = sat_ArrayAlloc(objectArray->num+1);
    size = objectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, objectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->obj, tv);
    }
  }

  if(cm->status == 0) {
    /* initialize option */
    option = sat_InitOption();
    option->cnfPrefix = bmcOption->cnfPrefix;
    /*option->verbose = bmcOption->verbosityLevel; */
    option->verbose = 0;
    option->timeoutLimit = bmcOption->timeOutPeriod;

    sat_SetIncrementalOption(option, bmcOption->incremental);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager, cm);
    /* value reset.. */
    sat_CleanDatabase(cm);
    /* set cone of influence */
    sat_SetConeOfInfluence(cm);
    sat_AllocLiteralsDB(cm);

    if(bmcOption->cnfFileName != NIL(char)) {
      sat_WriteCNF(cm, bmcOption->cnfFileName);
    }
    if(bmcOption->clauses == 0){ /* CirCUs circuit*/
      if (bmcOption->verbosityLevel == BmcVerbosityMax_c) {      
        fprintf(vis_stdout,
                "Number of Variables = %d Number of Clauses = %d\n",
                sat_GetNumberOfInitialVariables(cm),  sat_GetNumberOfInitialClauses(cm));
      }
      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
        (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
        (void) fflush(vis_stdout);
      }
      sat_Main(cm);
      if (bmcOption->verbosityLevel >= BmcVerbosityMax_c) {
        (void) fprintf(vis_stdout," done ");
        (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
      }
    }else if(bmcOption->clauses == 1) { /* CirCUs CNF */
      satArray_t *result;
      char       *fileName = NIL(char);
   
      sat_WriteCNF(cm, bmcOption->satInFile);
      if(bmcOption->satSolver == cusp){
        fileName = BmcCirCUsCallCusp(bmcOption);
      } else{ 
        if(bmcOption->satSolver == CirCUs){
          fileName = BmcCirCUsCallCirCUs(bmcOption);
        }
      }
      if(fileName != NIL(char)){
        satLevel_t *d;
        
        cm->status = SAT_SAT;
        result = sat_ReadForcedAssignment(fileName);
        d =  sat_AllocLevel(cm);
        sat_PutAssignmentValueMain(cm, d, result);
        sat_ArrayFree(result);
      } else {
        cm->status = SAT_UNSAT;
      }
    }
    /*sat_ReportStatistics(cm, cm->each);*/
  }
  sat_CombineStatistics(cm);

  if(interface == 0){
    interface = ALLOC(satInterface_t, 1);
  }
  interface->total = cm->total;
  interface->nonobjUnitLitArray = cm->nonobjUnitLitArray;
  interface->objUnitLitArray = 0;
  interface->savedConflictClauses = cm->savedConflictClauses;
  interface->trieArray = cm->trieArray;
  interface->status = cm->status;
  cm->total = 0;
  cm->nonobjUnitLitArray = 0;
  cm->savedConflictClauses = 0;

  if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
    manager->maxNodesArraySize = cm->maxNodesArraySize;
    manager->nameList   = REALLOC(char *, manager->nameList  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddIdArray = REALLOC(int ,   manager->bddIdArray  , manager->maxNodesArraySize/bAigNodeSize);
    manager->bddArray   = REALLOC(bdd_t *, manager->bddArray  , manager->maxNodesArraySize/bAigNodeSize);
  }
  manager->NodesArray = cm->nodesArray;
  manager->literals = cm->literals;

  /*
    For the case that the input contains CNF clauses;
  */
  if(cm->literals)
    cm->literals->last = cm->literals->initialSize;
  cm->nodesArray = 0;
  cm->HashTable = 0;
  cm->timeframe = 0;
  cm->timeframeWOI = 0;
  cm->literals = 0;

  sat_FreeManager(cm);

  return(interface);
}


satManager_t *
BmcCirCUsCreateManager(
  Ntk_Network_t *network)
{
  satManager_t *cm;
  bAig_Manager_t *manager;
  satOption_t *option;

  manager = Ntk_NetworkReadMAigManager(network);
  /* allocate sat manager*/
  cm = sat_InitManager(0);
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->nodesArray = manager->NodesArray;
  cm->HashTable = manager->HashTable;
  cm->literals = manager->literals;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdErr = vis_stderr;
  cm->stdOut = vis_stdout;
  cm->status = 0;
  cm->orderedVariableArray = 0;
  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);
  cm->option = 0;
  cm->each = 0;
  cm->decisionHead = 0;
  cm->variableArray = 0;
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  if(cm->status == 0) {
    /* initialize option*/
    option = sat_InitOption();
    /*option->verbose = bmcOption->verbosityLevel;*/
    option->verbose = 0;

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager, cm);
    /* value reset..*/
    sat_CleanDatabase(cm);
    /* set cone of influence*/
    sat_SetConeOfInfluence(cm);
    sat_AllocLiteralsDB(cm);

    /*sat_ReportStatistics(cm, cm->each);*/
  }
  sat_CombineStatistics(cm);

  /*
    For the case that the input contains CNF clauese;
  */
  if(cm->literals)
    cm->literals->last = cm->literals->initialSize;

  return(cm);
}
st_table *
BmcCirCUsGetCoiIndexTable(
        Ntk_Network_t *network,
        st_table *coiTable)
{
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t   *node;
  st_generator *gen;
  int          tmp;
  st_table     *node2MvfAigTable = 
    (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  int mvfSize, index, i;
  bAigEdge_t         v;
  MvfAig_Function_t  *mvfAig;
  st_table           *li2index, *coiIndexTable;
  
  assert(manager->timeframe != 0);
  /*
    Mohammad Says:
    This may solve the problem of calling expandTimeframe before calling this
    function. Check with HoonSang.
    
    if(timeframe == 0) 
    timeframe = bAig_InitTimeFrame(network, manager, 1);
  */
  
  /*
    li2index stores AIG id for inputs of all latches
   */
  li2index = manager->timeframe->li2index;
  coiIndexTable = st_init_table(st_numcmp, st_numhash);

  st_foreach_item_int(coiTable, gen, &node, &tmp) {
    if(!Ntk_NodeTestIsLatch(node))      continue;
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      if(st_lookup_int(li2index, (char *)v, &index)) 
        st_insert(coiIndexTable, (char *)(long)index, (char *)(long)index);
    }
  }
  return(coiIndexTable);
}

void
BmcRestoreAssertion(bAig_Manager_t *manager, satManager_t *cm)
{
int size, i, v;
array_t *asserted;

  if(manager->timeframe && manager->timeframe->assertedArray) {
    asserted = manager->timeframe->assertedArray;
    size = asserted->num;
    cm->assertion = sat_ArrayAlloc(size);
    for(i=0; i<size; i++) {
      v = array_fetch(int, asserted, i);
      sat_ArrayInsert(cm->assertion, v);
    }
  }
  else {
    cm->assertion = 0;
  }
}



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

static int
verifyIfConstant(
  bAigEdge_t   property)
{

  if (property == bAig_One){
    fprintf(vis_stdout,"# BMC: Empty counterexample because the property is always FALSE\n");
    fprintf(vis_stdout,"# BMC: formula failed\n");
    return 1;
  } else if (property == bAig_Zero){
    fprintf(vis_stdout,"# BMC: The property is always TRUE\n");
    fprintf(vis_stdout,"# BMC: formula passed\n");
    return 1;
  }
  return 0;
}