Major restructuring of the code.

4 files changed, 0 insertions, 4265 deletions

diff --git a/src/aig/live/liveness.c b/src/aig/live/liveness.c
deleted file mode 100644
index 324865a9..00000000
--- a/src/aig/live/liveness.c
+++ /dev/null
@@ -1,2575 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [liveness.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Liveness property checking.]
-
-  Synopsis    [Main implementation module.]
-
-  Author      [Sayak Ray]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2009.]
-
-  Revision    [$Id: liveness.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include "main.h"
-#include "aig.h"
-#include "saig.h"
-#include <string.h>
-#include "mainInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-#define PROPAGATE_NAMES
-#define MULTIPLE_LTL_FORMULA
-#define ALLOW_SAFETY_PROPERTIES
-
-#define FULL_BIERE_MODE 0
-#define IGNORE_LIVENESS_KEEP_SAFETY_MODE 1
-#define IGNORE_SAFETY_KEEP_LIVENESS_MODE 2
-#define IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE 3
-#define FULL_BIERE_ONE_LOOP_MODE 4
-//#define DUPLICATE_CKT_DEBUG
-
-extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-//char *strdup(const char *string);
-
-//******************************************
-//external functions defined in ltl_parser.c
-//******************************************
-typedef struct ltlNode_t ltlNode;
-extern ltlNode *readLtlFormula( char *formula );
-extern void traverseAbstractSyntaxTree( ltlNode *node );
-extern ltlNode *parseFormulaCreateAST( char *inputFormula );
-extern int isWellFormed( ltlNode *topNode );
-extern int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode );
-extern void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode );
-extern int checkAllBoolHaveAIGPointer( ltlNode *topASTNode );
-extern void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap );
-extern void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo );
-extern Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode );
-extern Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode );
-extern void traverseAbstractSyntaxTree_postFix( ltlNode *node );
-//**********************************
-//external function declaration ends
-//**********************************
-
- 
-/*******************************************************************
-LAYOUT OF PI VECTOR:
-
-+------------------------------------------------------------------------------------------------------------------------------------+
-| TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
-+------------------------------------------------------------------------------------------------------------------------------------+
-<------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->
-
-LAYOUT OF PO VECTOR:
-
-+-----------------------------------------------------------------------------------------------------------+
-| SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) |
-+-----------------------------------------------------------------------------------------------------------+
-<--True PO--->|<--------------------------------------LI---------------------------------------------------->
-
-********************************************************************/
-
-
-static int nodeName_starts_with( Abc_Obj_t *pNode, const char *prefix )
-{
-    if( strstr( Abc_ObjName( pNode ), prefix ) == Abc_ObjName( pNode ) )
-        return 1;
-    else
-        return 0;
-}
-
-void printVecPtrOfString( Vec_Ptr_t *vec )
-{
-    int i;
-
-    for( i=0; i< Vec_PtrSize( vec ); i++ )
-    {
-        printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
-    }
-}
-
-int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot )
-{
-    int i;
-    Aig_Obj_t *pObj;
-
-    Saig_ManForEachPo( pAig, pObj, i )
-    {
-        if( pObj == pPivot )
-            return i;
-    }
-    return -1;
-}
-
-char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot )
-{
-    Aig_Obj_t *pObjOld, *pObj;
-    Abc_Obj_t *pNode;
-    int index;
-
-    assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
-    Aig_ManForEachPi( pAigNew, pObj, index )
-        if( pObj == pObjPivot )
-            break;
-    assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
-    if( index == Saig_ManPiNum( pAigNew ) - 1 )
-        return "SAVE_BIERE";
-    else
-    {
-        pObjOld = Aig_ManPi( pAigOld, index );
-        pNode = Abc_NtkPi( pNtkOld, index );
-        assert( pObjOld->pData == pObjPivot );
-        return Abc_ObjName( pNode );
-    }
-}
-
-char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t * vFair )
-{
-    Aig_Obj_t *pObjOld, *pObj;
-    Abc_Obj_t *pNode;
-    int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
-    char *dummyStr = (char *)malloc( sizeof(char) * 50 );
-
-    assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
-    Saig_ManForEachLo( pAigNew, pObj, index )
-        if( pObj == pObjPivot )
-            break;
-    if( index < originalLatchNum )
-    {
-        oldIndex = Saig_ManPiNum( pAigOld ) + index;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
-        pNode = Abc_NtkCi( pNtkOld, oldIndex );
-        assert( pObjOld->pData == pObjPivot );
-        return Abc_ObjName( pNode );
-    }
-    else if( index == originalLatchNum )
-        return "SAVED_LO";
-    else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
-    {
-        oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
-        pNode = Abc_NtkCi( pNtkOld, oldIndex );
-        sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
-        return dummyStr;
-    }
-    else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
-    {
-        oldIndex = index - 2 * originalLatchNum - 1;
-        strMatch = 0;
-        dummyStr[0] = '\0';
-        Saig_ManForEachPo( pAigOld, pObj, i )
-        {
-            pNode = Abc_NtkPo( pNtkOld, i );
-            //if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
-            if(    nodeName_starts_with( pNode, "assert_fair" ) )
-            {
-                if( strMatch == oldIndex )
-                {
-                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
-                    //return dummyStr;
-                    break;
-                }
-                else
-                    strMatch++;
-            }
-        }
-        assert( dummyStr[0] != '\0' );
-        return dummyStr;
-    }
-    else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
-    {
-        oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
-        strMatch = 0;
-        dummyStr[0] = '\0';
-        Saig_ManForEachPo( pAigOld, pObj, i )
-        {
-            pNode = Abc_NtkPo( pNtkOld, i );
-            //if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
-            if(    nodeName_starts_with( pNode, "assume_fair" ) )
-            {
-                if( strMatch == oldIndex )
-                {
-                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
-                    //return dummyStr;
-                    break;
-                }
-                else
-                    strMatch++;
-            }
-        }
-        assert( dummyStr[0] != '\0' );
-        return dummyStr;
-    }
-    else
-        return "UNKNOWN";
-}
-
-Vec_Ptr_t *vecPis, *vecPiNames;
-Vec_Ptr_t *vecLos, *vecLoNames;
-
-
-int Aig_ManPiCleanupBiere( Aig_Man_t * p )
-{
-    int k = 0, nPisOld = Aig_ManPiNum(p);
-    
-    p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
-    if ( Aig_ManRegNum(p) )
-        p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
-    
-    return nPisOld - Aig_ManPiNum(p);
-}
-
-
-int Aig_ManPoCleanupBiere( Aig_Man_t * p )
-{
-    int k = 0, nPosOld = Aig_ManPoNum(p);
-
-    p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
-    if ( Aig_ManRegNum(p) )
-        p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
-    return nPosOld - Aig_ManPoNum(p);
-}
-
-Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
-                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
-{
-    Aig_Man_t * pNew;
-    int i, nRegCount;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
-    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
-    char *nodeName;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
-    
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-    //****************************************************************
-    // Step1: create the new manager
-    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-    // nodes, but this selection is arbitrary - need to be justified
-    //****************************************************************
-    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
-    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
-    pNew->pSpec = NULL;
-    
-    //****************************************************************
-    // Step 2: map constant nodes
-    //****************************************************************
-    pObj = Aig_ManConst1( p );
-    pObj->pData = Aig_ManConst1( pNew );
-
-    //****************************************************************
-    // Step 3: create true PIs
-    //****************************************************************
-    Saig_ManForEachPi( p, pObj, i )
-    {
-        piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecPis, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 4: create the special Pi corresponding to SAVE
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
-        nodeName = "SAVE_BIERE",
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-        
-    //****************************************************************
-    // Step 5: create register outputs
-    //****************************************************************
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecLos, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 6: create "saved" register output
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        loCreated++;
-        pObjSavedLo = Aig_ObjCreatePi( pNew );
-        Vec_PtrPush( vecLos, pObjSavedLo );
-        nodeName = "SAVED_LO";
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-    }
-
-    //********************************************************************
-    // Step 8: create internal nodes
-    //********************************************************************
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    }
-
-    
-    //********************************************************************
-    // Step 8.x : create PO for each safety assertions
-    // NOTE : Here the output is purposely inverted as it will be thrown to 
-    // dprove
-    //********************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-    {
-        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
-        {
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
-        }
-        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
-        {
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            collectiveAssertSafety = pObjAndAcc;
-
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            collectiveAssumeSafety = pObjAndAcc;
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
-        }
-        else
-        {
-            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
-            pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
-        }
-    }
-
-    //********************************************************************
-    // Step 9: create the safety property output gate for the liveness properties
-    // discuss with Sat/Alan for an alternative implementation
-    //********************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-    }
-
-    // create register inputs for the original registers
-    nRegCount = 0;
-    
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pMatch = Saig_ObjLoToLi( p, pObj );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-        nRegCount++;
-        liCopied++;
-    }
-
-    // create register input corresponding to the register "saved"
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        #ifndef DUPLICATE_CKT_DEBUG
-            pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-            nRegCount++;
-            liCreated++;
-
-            //Changed on October 13, 2009
-            //pObjAndAcc = NULL;
-            pObjAndAcc = Aig_ManConst1( pNew );
-
-    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
-            Saig_ManForEachLo( p, pObj, i )
-            {
-                pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                #ifdef PROPAGATE_NAMES
-                    Vec_PtrPush( vecLos, pObjShadowLo );
-                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
-                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
-                    
-                    Vec_PtrPush( vecLoNames, nodeName );
-                #endif
-
-                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                nRegCount++;
-                loCreated++; liCreated++;
-        
-                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjXnor = Aig_Not( pObjXor );
-                
-                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
-            }
-
-            // create the AND gate whose output will be the signal "looped"
-            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
-
-            // create the master AND gate and corresponding AND and OR logic for the liveness properties
-            pObjAndAcc = Aig_ManConst1( pNew );
-            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
-            {
-                printf("Circuit without any liveness property\n");
-            }
-            else
-            {
-                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
-                {
-                    liveLatch++;
-                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                    #ifdef PROPAGATE_NAMES
-                        Vec_PtrPush( vecLos, pObjShadowLo );
-                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
-                        Vec_PtrPush( vecLoNames, nodeName );
-                    #endif
-
-                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                    nRegCount++;
-                    loCreated++; liCreated++;
-            
-                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
-                }
-            }
-
-            pObjLive = pObjAndAcc;
-                
-            pObjAndAcc = Aig_ManConst1( pNew );
-            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
-                printf("Circuit without any fairness property\n");
-            else
-            {
-                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
-                {
-                    fairLatch++;
-                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                    #ifdef PROPAGATE_NAMES
-                        Vec_PtrPush( vecLos, pObjShadowLo );
-                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
-                        Vec_PtrPush( vecLoNames, nodeName );
-                    #endif
-
-                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                    nRegCount++;
-                    loCreated++; liCreated++;
-            
-                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
-                }
-            }
-
-            pObjFair = pObjAndAcc;
-                
-            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
-            //Following is the actual Biere translation
-            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
-
-            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-        #endif
-    }
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-    
-    Aig_ManCleanup( pNew );
-    
-    assert( Aig_ManCheck( pNew ) );
-    
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
-            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
-            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
-    }
-
-    return pNew;
-}
-
-
-
-
-
-Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Int_t *vFlops, 
-                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
-{
-    Aig_Man_t * pNew;
-    int i, nRegCount, iEntry;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
-    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
-    char *nodeName;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
-    
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-    //****************************************************************
-    // Step1: create the new manager
-    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-    // nodes, but this selection is arbitrary - need to be justified
-    //****************************************************************
-    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-    pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l2s") + 1 );
-    sprintf(pNew->pName, "%s_%s", pNtk->pName, "l2s");
-    pNew->pSpec = NULL;
-    
-    //****************************************************************
-    // Step 2: map constant nodes
-    //****************************************************************
-    pObj = Aig_ManConst1( p );
-    pObj->pData = Aig_ManConst1( pNew );
-
-    //****************************************************************
-    // Step 3: create true PIs
-    //****************************************************************
-    Saig_ManForEachPi( p, pObj, i )
-    {
-        piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecPis, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 4: create the special Pi corresponding to SAVE
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
-        nodeName = "SAVE_BIERE",
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-        
-    //****************************************************************
-    // Step 5: create register outputs
-    //****************************************************************
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecLos, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 6: create "saved" register output
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        loCreated++;
-        pObjSavedLo = Aig_ObjCreatePi( pNew );
-        Vec_PtrPush( vecLos, pObjSavedLo );
-        nodeName = "SAVED_LO";
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-    //****************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-        pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-    }
-
-    //********************************************************************
-    // Step 8: create internal nodes
-    //********************************************************************
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    }
-
-    
-    //********************************************************************
-    // Step 8.x : create PO for each safety assertions
-    // NOTE : Here the output is purposely inverted as it will be thrown to 
-    // dprove
-    //********************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-    {
-        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
-        {
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
-        }
-        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
-        {
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            collectiveAssertSafety = pObjAndAcc;
-
-            pObjAndAcc = Aig_ManConst1( pNew );
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
-            {
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-            }
-            collectiveAssumeSafety = pObjAndAcc;
-            Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
-        }
-        else
-        {
-            printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
-            Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
-        }
-    }
-
-    //********************************************************************
-    // Step 9: create the safety property output gate for the liveness properties
-    // discuss with Sat/Alan for an alternative implementation
-    //********************************************************************
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-    }
-
-    // create register inputs for the original registers
-    nRegCount = 0;
-    
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pMatch = Saig_ObjLoToLi( p, pObj );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-        nRegCount++;
-        liCopied++;
-    }
-
-    // create register input corresponding to the register "saved"
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        #ifndef DUPLICATE_CKT_DEBUG
-            pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-            nRegCount++;
-            liCreated++;
-
-            //Changed on October 13, 2009
-            //pObjAndAcc = NULL;
-            pObjAndAcc = Aig_ManConst1( pNew );
-
-    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
-            //Saig_ManForEachLo( p, pObj, i )
-            Saig_ManForEachLo( p, pObj, i )
-            {
-                printf("Flop[%d] = %s\n", i, Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) );
-            }
-            Vec_IntForEachEntry( vFlops, iEntry, i )
-            {
-                pObjShadowLo = Aig_ObjCreatePi( pNew );
-                pObj = Aig_ManLo( p, iEntry );
-
-                #ifdef PROPAGATE_NAMES
-                    Vec_PtrPush( vecLos, pObjShadowLo );
-                    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ) ) + 10 );
-                    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + iEntry ) ), "SHADOW" );
-                    printf("Flop copied [%d] = %s\n", iEntry, nodeName );
-                    Vec_PtrPush( vecLoNames, nodeName );
-                #endif
-
-                pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                nRegCount++;
-                loCreated++; liCreated++;
-        
-                pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                pObjXnor = Aig_Not( pObjXor );
-                
-                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
-            }
-
-            // create the AND gate whose output will be the signal "looped"
-            pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
-
-            // create the master AND gate and corresponding AND and OR logic for the liveness properties
-            pObjAndAcc = Aig_ManConst1( pNew );
-            if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
-            {
-                printf("Circuit without any liveness property\n");
-            }
-            else
-            {
-                Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
-                {
-                    liveLatch++;
-                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                    #ifdef PROPAGATE_NAMES
-                        Vec_PtrPush( vecLos, pObjShadowLo );
-                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
-                        Vec_PtrPush( vecLoNames, nodeName );
-                    #endif
-
-                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                    nRegCount++;
-                    loCreated++; liCreated++;
-            
-                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
-                }
-            }
-
-            pObjLive = pObjAndAcc;
-                
-            pObjAndAcc = Aig_ManConst1( pNew );
-            if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
-                printf("Circuit without any fairness property\n");
-            else
-            {
-                Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
-                {
-                    fairLatch++;
-                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                    #ifdef PROPAGATE_NAMES
-                        Vec_PtrPush( vecLos, pObjShadowLo );
-                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
-                        Vec_PtrPush( vecLoNames, nodeName );
-                    #endif
-
-                    pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                    pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                    nRegCount++;
-                    loCreated++; liCreated++;
-            
-                    pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAcc );
-                }
-            }
-
-            pObjFair = pObjAndAcc;
-                
-            //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
-            //Following is the actual Biere translation
-            pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
-
-            Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-        #endif
-    }
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-    
-    Aig_ManCleanup( pNew );
-    
-    assert( Aig_ManCheck( pNew ) );
-    
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
-            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
-            assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
-    }
-
-    return pNew;
-}
-
-
-
-Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
-                                                      Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety )
-{
-    Aig_Man_t * pNew;
-    int i, nRegCount;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
-    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage;
-    Aig_Obj_t *pObjCorrespondingLi;
-    Aig_Obj_t *pArgument;
-    Aig_Obj_t *collectiveAssertSafety, *collectiveAssumeSafety;
-
-    char *nodeName;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0;
-
-    if( Aig_ManRegNum( p ) == 0 )
-    {
-        printf("The input AIG contains no register, returning the original AIG as it is\n");
-        return p;
-    }
-
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-    //****************************************************************
-    // Step1: create the new manager
-    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-    // nodes, but this selection is arbitrary - need to be justified
-    //****************************************************************
-    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( "live2safe" );
-    pNew->pSpec = NULL;
-    
-    //****************************************************************
-    // Step 2: map constant nodes
-    //****************************************************************
-    pObj = Aig_ManConst1( p );
-    pObj->pData = Aig_ManConst1( pNew );
-
-    //****************************************************************
-    // Step 3: create true PIs
-    //****************************************************************
-    Saig_ManForEachPi( p, pObj, i )
-    {
-        piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecPis, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 4: create the special Pi corresponding to SAVE
-    //****************************************************************
-    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
-    {
-        pObjSavePi = Aig_ObjCreatePi( pNew );
-        nodeName = "SAVE_BIERE",
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-            
-    //****************************************************************
-    // Step 5: create register outputs
-    //****************************************************************
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecLos, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 6: create "saved" register output
-    //****************************************************************
-
-#if 0
-    loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
-    Vec_PtrPush( vecLos, pObjSavedLo );
-    nodeName = "SAVED_LO";
-    Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-    //****************************************************************
-    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-    //****************************************************************
-#if 0
-    pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-    pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-#endif
-
-    //********************************************************************
-    // Step 8: create internal nodes
-    //********************************************************************
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    }
-
-#if 0
-    //********************************************************************
-    // Step 8.x : create PO for each safety assertions
-    //********************************************************************
-    Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-    {
-        pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
-    }
-#endif
-
-    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-    {
-        if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
-        {
-            pObjAndAcc = NULL;
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                if( pObjAndAcc == NULL )
-                    pObjAndAcc = pArgument;
-                else
-                {
-                    pObjAndAccDummy = pObjAndAcc;
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
-                }
-            }
-            Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
-        }
-        else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
-        {
-            pObjAndAcc = NULL;
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-            {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                if( pObjAndAcc == NULL )
-                    pObjAndAcc = pArgument;
-                else
-                {
-                    pObjAndAccDummy = pObjAndAcc;
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
-                }
-            }
-            collectiveAssertSafety = pObjAndAcc;
-            pObjAndAcc = NULL;
-            Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
-            {
-                //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) );
-                pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                if( pObjAndAcc == NULL )
-                    pObjAndAcc = pArgument;
-                else
-                {
-                    pObjAndAccDummy = pObjAndAcc;
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy );
-                }
-            }
-            collectiveAssumeSafety = pObjAndAcc;
-            Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
-        }
-        else
-            printf("No safety property is specified, hence no safety gate is created\n");
-    }
-
-    //********************************************************************
-    // Step 9: create the safety property output gate
-    // create the safety property output gate, this will be the sole true PO 
-    // of the whole circuit, discuss with Sat/Alan for an alternative implementation
-    //********************************************************************
-
-    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
-    {
-        pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-    }
-
-    // create register inputs for the original registers
-    nRegCount = 0;
-    
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-        nRegCount++;
-        liCopied++;
-    }
-
-#if 0
-    // create register input corresponding to the register "saved"
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-    nRegCount++;
-    liCreated++;7
-#endif
-
-    pObjAndAcc = NULL;
-
-    //****************************************************************************************************
-    //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
-    //between Lo_j and Li_j and then a cascade of AND gates
-    //****************************************************************************************************
-
-    if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE )
-    {
-        Saig_ManForEachLo( p, pObj, i )
-        {
-            pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
-        
-            pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData,  Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
-            pObjXnor = Aig_Not( pObjXor );
-        
-            if( pObjAndAcc == NULL )
-                pObjAndAcc = pObjXnor;
-            else
-            {
-                pObjAndAccDummy = pObjAndAcc;
-                pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
-            }
-        }
-
-        // create the AND gate whose output will be the signal "looped"
-        pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
-    
-        // create the master AND gate and corresponding AND and OR logic for the liveness properties
-        pObjAndAcc = NULL;
-        if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
-            printf("Circuit without any liveness property\n");
-        else
-        {
-            Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
-            {
-                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                if( pObjAndAcc == NULL )
-                    pObjAndAcc = pDriverImage;
-                else
-                {
-                    pObjAndAccDummy = pObjAndAcc;
-                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
-                }
-            }
-        }
-
-        if( pObjAndAcc != NULL )
-            pObjLive = pObjAndAcc;
-        else
-            pObjLive = Aig_ManConst1( pNew );
-    
-        // create the master AND gate and corresponding AND and OR logic for the fairness properties
-        pObjAndAcc = NULL;
-        if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
-            printf("Circuit without any fairness property\n");
-        else
-        {
-            Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
-            {
-                pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                if( pObjAndAcc == NULL )
-                    pObjAndAcc = pDriverImage;
-                else
-                {
-                    pObjAndAccDummy = pObjAndAcc;
-                    pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
-                }
-            }
-        }
-
-        if( pObjAndAcc != NULL )
-            pObjFair = pObjAndAcc;
-        else
-            pObjFair = Aig_ManConst1( pNew );
-    
-        pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
-    
-        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-    }
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-
-    Aig_ManCleanup( pNew );
-    
-    assert( Aig_ManCheck( pNew ) );
-    
-    return pNew;
-}
-
-
-
-Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, liveCounter = 0;
-    Vec_Ptr_t * vLive;
-
-    vLive = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
-        if( nodeName_starts_with( pNode, "assert_fair" ) )
-        {
-            Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) );
-            liveCounter++;
-        }
-    printf("Number of liveness property found = %d\n", liveCounter);
-    return vLive;
-}
-
-Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, fairCounter = 0;
-    Vec_Ptr_t * vFair;
-
-    vFair = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
-        if( nodeName_starts_with( pNode, "assume_fair" ) )
-        {
-            Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) );
-            fairCounter++;
-        }
-    printf("Number of fairness property found = %d\n", fairCounter);
-    return vFair;
-}
-
-Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, assertSafetyCounter = 0;
-    Vec_Ptr_t * vAssertSafety;
-
-    vAssertSafety = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
-        if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" ))
-        {
-            Vec_PtrPush( vAssertSafety, Aig_ManPo( pAig, i ) );
-            assertSafetyCounter++;
-        }
-    printf("Number of safety property found = %d\n", assertSafetyCounter);
-    return vAssertSafety;
-}
-
-Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, assumeSafetyCounter = 0;
-    Vec_Ptr_t * vAssumeSafety;
-
-    vAssumeSafety = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL )
-        if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" ))
-        {
-            Vec_PtrPush( vAssumeSafety, Aig_ManPo( pAig, i ) );
-            assumeSafetyCounter++;
-        }
-    printf("Number of assume_safety property found = %d\n", assumeSafetyCounter);
-    return vAssumeSafety;
-}
-
-void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames )
-{
-    Aig_Obj_t *pObj;
-    Abc_Obj_t *pNode;
-    int i, ntkObjId;
-
-    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
-
-    if( vPiNames )
-    {
-        Saig_ManForEachPi( pAig, pObj, i )
-        {
-            ntkObjId = Abc_NtkCi( pNtk, i )->Id;
-            //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);  
-            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
-        }
-    }
-    if( vLoNames )
-    {
-        Saig_ManForEachLo( pAig, pObj, i )
-        {
-            ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
-            //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);  
-            Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
-        }
-    }
-
-    Abc_NtkForEachPo(pNtk, pNode, i)
-    {
-        Abc_ObjAssignName(pNode, "assert_safety_", Abc_ObjName(pNode) );
-    }
-
-    // assign latch input names
-    Abc_NtkForEachLatch(pNtk, pNode, i)
-        if ( Nm_ManFindNameById(pNtk->pManName, Abc_ObjFanin0(pNode)->Id) == NULL )
-            Abc_ObjAssignName( Abc_ObjFanin0(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)), NULL );
-}
-
-
-int Abc_CommandAbcLivenessToSafety( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
-    Aig_Man_t * pAig, *pAigNew;
-    int c;
-    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
-    int directive = -1;
-                
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    if( argc == 1 )
-    {
-        assert( directive == -1 );
-        directive = FULL_BIERE_MODE;
-    }
-    else
-    {
-        Extra_UtilGetoptReset();
-        while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
-        {
-            switch( c )
-            {
-            case '1': 
-                if( directive == -1 )
-                    directive = FULL_BIERE_ONE_LOOP_MODE;
-                else
-                {
-                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
-                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                    else
-                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 's':
-                if( directive == -1 )
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 'l':
-                if( directive == -1 )
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                }
-                break;
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-            }
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-    if( !Abc_NtkIsStrash( pNtk ) )
-    {
-        printf("The input network was not strashed, strashing....\n");
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkOld = pNtkTemp;
-        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-    else
-    {
-        pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNtkOld = pNtk;
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-
-    switch( directive )
-    {
-    case FULL_BIERE_MODE:
-        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
-        //{
-        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case FULL_BIERE_ONE_LOOP_MODE:
-        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
-        //{
-        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
-        //if( Vec_PtrSize(vAssertSafety) == 0 )
-        //{    
-        //    printf("Input circuit has NO safety property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
-        //if( Vec_PtrSize(vLive) == 0 )
-        //{    
-        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
-        //if( Vec_PtrSize(vLive) == 0 )
-        //{
-        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
-            break;
-        //}
-    }
-
-#if 0
-    if( argc == 1 )
-    {
-        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-        if( Aig_ManRegNum(pAigNew) != 0 )
-            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
-    }
-    else 
-    {
-        Extra_UtilGetoptReset();
-        c = Extra_UtilGetopt( argc, argv, "1lsh" );
-        if( c == '1' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-        }
-        else if( c == 'l' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
-        }
-        else if( c == 's' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
-        }
-        else if( c == 'h' )
-            goto usage;
-        else
-            goto usage;
-    }
-#endif
-    
-#if 0
-    Aig_ManPrintStats( pAigNew );
-    printf("\nDetail statistics*************************************\n");
-    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
-    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
-    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
-    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
-    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
-    printf("\n*******************************************************\n");
-#endif
-
-    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
-    pNtkNew->pName = Aig_UtilStrsav( pAigNew->pName );
-    
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
-    
-    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
-    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
-
-#if 0
-#ifndef DUPLICATE_CKT_DEBUG
-    Saig_ManForEachPi( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
-        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
-
-    Saig_ManForEachLo( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
-#endif    
-#endif
-        
-    return 0;
-
-usage:
-    fprintf( stdout, "usage: l2s [-1lsh]\n" );
-    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
-    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
-    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
-    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
-    fprintf( stdout, "\t-h : print command usage\n");
-    return 1;
-}
-
-Vec_Int_t * prepareFlopVector( Aig_Man_t * pAig, int vectorLength )
-{
-    Vec_Int_t *vFlops;
-    int i;
-
-    vFlops = Vec_IntAlloc( vectorLength );
-
-    for( i=0; i<vectorLength; i++ )
-        Vec_IntPush( vFlops, i );
-
-#if 0
-    Vec_IntPush( vFlops, 19 );
-    Vec_IntPush( vFlops, 20 );
-    Vec_IntPush( vFlops, 23 );
-    Vec_IntPush( vFlops, 24 );
-    //Vec_IntPush( vFlops, 2 );
-    //Vec_IntPush( vFlops, 3 );
-    //Vec_IntPush( vFlops, 4 );
-    //Vec_IntPush( vFlops, 5 );
-    //Vec_IntPush( vFlops, 8 );
-    //Vec_IntPush( vFlops, 9 );
-    //Vec_IntPush( vFlops, 10 );
-    //Vec_IntPush( vFlops, 11 );
-    //Vec_IntPush( vFlops, 0 );
-    //Vec_IntPush( vFlops, 0 );
-#endif
-
-    return vFlops;
-}
-
-int Abc_CommandAbcLivenessToSafetyAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
-    Aig_Man_t * pAig, *pAigNew;
-    int c;
-    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
-    int directive = -1;
-    Vec_Int_t * vFlops;
-                
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    if( argc == 1 )
-    {
-        assert( directive == -1 );
-        directive = FULL_BIERE_MODE;
-    }
-    else
-    {
-        Extra_UtilGetoptReset();
-        while ( ( c = Extra_UtilGetopt( argc, argv, "1slh" ) ) != EOF )
-        {
-            switch( c )
-            {
-            case '1': 
-                if( directive == -1 )
-                    directive = FULL_BIERE_ONE_LOOP_MODE;
-                else
-                {
-                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
-                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                    else
-                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 's':
-                if( directive == -1 )
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 'l':
-                if( directive == -1 )
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                }
-                break;
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-            }
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-    if( !Abc_NtkIsStrash( pNtk ) )
-    {
-        printf("The input network was not strashed, strashing....\n");
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkOld = pNtkTemp;
-        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-    else
-    {
-        pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNtkOld = pNtk;
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-
-    vFlops = prepareFlopVector( pAig, Aig_ManRegNum(pAig)%2 == 0? Aig_ManRegNum(pAig)/2 : (Aig_ManRegNum(pAig)-1)/2);
-
-    //vFlops = prepareFlopVector( pAig, 100 );
-
-    switch( directive )
-    {
-    case FULL_BIERE_MODE:
-        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
-        //{
-        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationAbs( FULL_BIERE_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case FULL_BIERE_ONE_LOOP_MODE:
-        //if( Vec_PtrSize(vLive) == 0 && Vec_PtrSize(vAssertSafety) == 0 )
-        //{
-        //    printf("Input circuit has NO safety and NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
-        //if( Vec_PtrSize(vAssertSafety) == 0 )
-        //{    
-        //    printf("Input circuit has NO safety property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationAbs( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
-        //if( Vec_PtrSize(vLive) == 0 )
-        //{    
-        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationAbs( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vFlops, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t1 PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n");
-            break;
-        //}
-    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
-        //if( Vec_PtrSize(vLive) == 0 )
-        //{
-        //    printf("Input circuit has NO liveness property, original network is not disturbed\n");
-        //    return 1;
-        //}
-        //else
-        //{
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
-            break;
-        //}
-    }
-
-    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
-    pNtkNew->pName = Aig_UtilStrsav( pAigNew->pName );
-    
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
-    
-    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
-    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
-
-#if 0
-#ifndef DUPLICATE_CKT_DEBUG
-    Saig_ManForEachPi( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
-        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
-
-    Saig_ManForEachLo( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
-#endif    
-#endif
-        
-    return 0;
-
-usage:
-    fprintf( stdout, "usage: l2s [-1lsh]\n" );
-    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
-    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
-    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
-    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
-    fprintf( stdout, "\t-h : print command usage\n");
-    return 1;
-}
-
-Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, 
-                                           Vec_Ptr_t *vLive, Vec_Ptr_t *vFair, Vec_Ptr_t *vAssertSafety, Vec_Ptr_t *vAssumeSafety,
-                                           int *numLtlProcessed, Vec_Ptr_t *ltlBuffer )
-{
-    Aig_Man_t * pNew;
-    int i, ii, iii, nRegCount;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSaveOrSaved, *pObjSaveAndNotSaved, *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc;
-    Aig_Obj_t *pObjLive, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pObjOriginalSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage, *pArgument, *collectiveAssertSafety, *collectiveAssumeSafety;
-    Aig_Obj_t *pNegatedSafetyConjunction = NULL;
-    Aig_Obj_t *pObjSafetyAndLiveToSafety;
-    char *nodeName, *pFormula;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
-    Vec_Ptr_t *vSignal, *vTopASTNodeArray;
-    ltlNode *pEnrtyGLOBALLY;
-    ltlNode *topNodeOfAST, *tempTopASTNode;
-    Vec_Vec_t *vAigGFMap;
-    Vec_Ptr_t *vSignalMemory, *vGFFlopMemory, *vPoForLtlProps;
-    Vec_Ptr_t *vecInputLtlFormulae;
-    
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-    //****************************************************************
-    //step0: Parsing the LTL formula
-    //****************************************************************
-    //Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pFormula, i )
-    //    printf("\ninput LTL formula [%d] = %s\n", i, pFormula );
-
-
-#ifdef MULTIPLE_LTL_FORMULA
-
-
-    //***************************************************************************
-    //Reading input LTL formulae from Ntk data-structure and creating 
-    //AST for them, Steps involved: 
-    //        parsing -> AST creation -> well-formedness check -> signal name check
-    //***************************************************************************
-
-    //resetting numLtlProcessed
-    *numLtlProcessed = 0;
-    
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-        //if( ltlBuffer )
-        vecInputLtlFormulae = ltlBuffer;
-        //vecInputLtlFormulae = pNtk->vLtlProperties;
-        if( vecInputLtlFormulae )
-        {
-            vTopASTNodeArray = Vec_PtrAlloc( Vec_PtrSize( vecInputLtlFormulae ) );
-            printf("\n");
-            Vec_PtrForEachEntry( char *, vecInputLtlFormulae, pFormula, i )
-            {
-                tempTopASTNode = parseFormulaCreateAST( pFormula );
-                //traverseAbstractSyntaxTree_postFix( tempTopASTNode );
-                if( tempTopASTNode )
-                {
-                    printf("Formula %d: AST is created, ", i+1);
-                    if( isWellFormed( tempTopASTNode ) )
-                        printf("Well-formedness check PASSED, ");
-                    else
-                    {
-                        printf("Well-formedness check FAILED!!\n");
-                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
-                        //do memory management to free the created AST
-                        continue;
-                    }
-                    if( checkSignalNameExistence( pNtk, tempTopASTNode ) )
-                        printf("Signal check PASSED\n");
-                    else
-                    {
-                        printf("Signal check FAILED!!");
-                        printf("AST will be ignored for formula %d, no extra logic will be added for this formula\n", i+1 );
-                        //do memory management to free the created AST
-                        continue;
-                    }
-                    Vec_PtrPush( vTopASTNodeArray, tempTopASTNode );
-                    (*numLtlProcessed)++;
-                }
-                else
-                    printf("\nNo AST has been created for formula %d, no extra logic will be added\n", i+1 );
-            }
-        }
-        printf("\n");
-        if( Vec_PtrSize( vTopASTNodeArray ) == 0 )
-        {
-            //printf("\nNo AST has been created for any formula; hence the circuit is left untouched\n");
-            printf("\nCurrently aborting, need to take care when Vec_PtrSize( vTopASTNodeArray ) == 0\n");
-            exit(0);
-        }
-    }
-
-        //****************************************************************
-        // Step1: create the new manager
-        // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-        // nodes, but this selection is arbitrary - need to be justified
-        //****************************************************************
-        pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-        pNew->pName = (char *)malloc( strlen( pNtk->pName ) + strlen("_l3s") + 1 );
-        sprintf(pNew->pName, "%s_%s", pNtk->pName, "l3s");
-        pNew->pSpec = NULL;
-    
-        //****************************************************************
-        // Step 2: map constant nodes
-        //****************************************************************
-        pObj = Aig_ManConst1( p );
-        pObj->pData = Aig_ManConst1( pNew );
-
-        //****************************************************************
-        // Step 3: create true PIs
-        //****************************************************************
-        Saig_ManForEachPi( p, pObj, i )
-        {
-            piCopied++;
-            pObj->pData = Aig_ObjCreatePi(pNew);
-            Vec_PtrPush( vecPis, pObj->pData );
-            nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-            Vec_PtrPush( vecPiNames, nodeName );
-        }
-
-        //****************************************************************
-        // Step 4: create the special Pi corresponding to SAVE
-        //****************************************************************
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-        {
-            pObjSavePi = Aig_ObjCreatePi( pNew );
-            nodeName = "SAVE_BIERE",
-            Vec_PtrPush( vecPiNames, nodeName );
-        }
-        
-        //****************************************************************
-        // Step 5: create register outputs
-        //****************************************************************
-        Saig_ManForEachLo( p, pObj, i )
-        {
-            loCopied++;
-            pObj->pData = Aig_ObjCreatePi(pNew);
-            Vec_PtrPush( vecLos, pObj->pData );
-            nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-            Vec_PtrPush( vecLoNames, nodeName );
-        }
-
-        //****************************************************************
-        // Step 6: create "saved" register output
-        //****************************************************************
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-        {
-            loCreated++;
-            pObjSavedLo = Aig_ObjCreatePi( pNew );
-            Vec_PtrPush( vecLos, pObjSavedLo );
-            nodeName = "SAVED_LO";
-            Vec_PtrPush( vecLoNames, nodeName );
-        }
-
-        //****************************************************************
-        // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-        //****************************************************************
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-        {
-            pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-            pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-        }
-
-        //********************************************************************
-        // Step 8: create internal nodes
-        //********************************************************************
-        Aig_ManForEachNode( p, pObj, i )
-        {
-            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        }
-
-        
-        //********************************************************************
-        // Step 8.x : create PO for each safety assertions
-        // NOTE : Here the output is purposely inverted as it will be thrown to 
-        // dprove
-        //********************************************************************
-        assert( pNegatedSafetyConjunction == NULL );
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE)
-        {
-            if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) == 0 )
-            {
-                pObjAndAcc = Aig_ManConst1( pNew );
-                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-                {
-                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-                }
-                pNegatedSafetyConjunction = Aig_Not(pObjAndAcc);
-                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) );
-            }
-            else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 )
-            {
-                pObjAndAcc = Aig_ManConst1( pNew );
-                Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i )
-                {
-                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-                }
-                collectiveAssertSafety = pObjAndAcc;
-
-                pObjAndAcc = Aig_ManConst1( pNew );
-                Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i )
-                {
-                    pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) );
-                    pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc );
-                }
-                collectiveAssumeSafety = pObjAndAcc;
-                pNegatedSafetyConjunction =  Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety );
-                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) );
-            }
-            else
-            {
-                printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n");
-                pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) );
-                if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                    pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) );
-            }
-        }
-        assert( pNegatedSafetyConjunction != NULL );
-
-        //********************************************************************
-        // Step 9: create the safety property output gate for the liveness properties
-        // discuss with Sat/Alan for an alternative implementation
-        //********************************************************************
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-        {
-            vPoForLtlProps = Vec_PtrAlloc( Vec_PtrSize( vTopASTNodeArray ) );
-            if( Vec_PtrSize( vTopASTNodeArray ) )
-            {
-                //no effective AST for any input LTL property
-                //must do something graceful
-            }
-            for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ )
-            {
-                pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-                Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput );
-            }
-        }
-
-        //*************************************************************************************
-        // Step 10: Placeholder PO's were created for Liveness property outputs in the
-        // last step. FYI, # of new liveness property outputs = # of LTL properties in the circuit
-        // It is time for creation of loop LI's and other stuff
-        // Now creating register inputs for the original flops
-        //*************************************************************************************
-        nRegCount = 0;
-        
-        Saig_ManForEachLo( p, pObj, i )
-        {
-            pMatch = Saig_ObjLoToLi( p, pObj );
-            Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-            nRegCount++;
-            liCopied++;
-        }
-
-        //*************************************************************************************
-        // Step 11: create register input corresponding to the register "saved"
-        //*************************************************************************************
-        if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-        {
-            #ifndef DUPLICATE_CKT_DEBUG
-                pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-                nRegCount++;
-                liCreated++;
-
-                pObjAndAcc = Aig_ManConst1( pNew );
-
-                //*************************************************************************************
-                // Step 11: create the family of shadow registers, then create the cascade of Xnor 
-                // and And gates for the comparator 
-                //*************************************************************************************
-                Saig_ManForEachLo( p, pObj, i )
-                {
-                //printf("\nKEMON RENDY = %s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i )) );
-                //top|route0_target0_queue_with_credit0_queue0
-                //top|route0_master0_queue2
-                //    if( strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 
-                //            || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp(  Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 )
-                    {        
-                        pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-                    #ifdef PROPAGATE_NAMES
-                        Vec_PtrPush( vecLos, pObjShadowLo );
-                        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
-                        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
-                        
-                        Vec_PtrPush( vecLoNames, nodeName );
-                    #endif
-
-                        pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                        pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-                        nRegCount++;
-                        loCreated++; liCreated++;
-            
-                        pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-                        pObjXnor = Aig_Not( pObjXor );
-                    
-                        pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAcc );
-                    }
-                }
-
-                // create the AND gate whose output will be the signal "looped"
-                pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
-
-                // create the master AND gate and corresponding AND and OR logic for the liveness properties
-                
-                //*************************************************************************************
-                // Step 11: logic for LTL properties:- (looped & ~theta) where theta is the input ltl 
-                // property
-                // Description of some data-structure:
-                //-------------------------------------------------------------------------------------
-                // Name          | Type            | Purpose
-                //-------------------------------------------------------------------------------------
-                // vSignalMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
-                //                 |                   | It remembers if OR+Latch for GF node has already been
-                //                 |                   | created for a particular signal.
-                //               |                 |
-                // vGFFlopMemory | Vec_Ptr_t *     | A vector across all ASTs of the LTL properties
-                //                 |                 | remembers if OR+Latch of a GF node has already been created
-                //                 |                 |
-                // vSignal         | Vec_Ptr_t *     | vector for each AST; contains pointers from GF nodes
-                //               |                 | to AIG signals
-                //                 |                   |
-                // vAigGFMap     | Vec_Vec_t *     | vAigGFMap[ index ] = vector of GF nodes pointing to
-                //               |                 | the same AIG node; "index" is the index of that
-                //               |                 | AIG node in the vector vSignal
-                //*************************************************************************************
-                
-                vSignalMemory = Vec_PtrAlloc(10);
-                vGFFlopMemory = Vec_PtrAlloc(10);
-
-                Vec_PtrForEachEntry( ltlNode *, vTopASTNodeArray, topNodeOfAST, iii )
-                {
-                                    vSignal = Vec_PtrAlloc( 10 );
-                                    vAigGFMap = Vec_VecAlloc( 10 );
-                                    
-                                    //*************************************************************************************
-                                    //Step 11a: for the current AST, find out the leaf level Boolean signal pointers from 
-                                    // the NEW aig.
-                                    //*************************************************************************************
-                                    populateBoolWithAigNodePtr( pNtk, p, pNew, topNodeOfAST );
-                                    assert( checkAllBoolHaveAIGPointer( topNodeOfAST ) );
-
-                                    //*************************************************************************************
-                                    //Step 11b: for each GF node, compute the pointer in AIG that it should point to
-                                    // In particular, if the subtree below GF is some Boolean crown (including the case
-                                    // of simple negation, create new logic and populate the AIG pointer in GF node
-                                    // accordingly
-                                    //*************************************************************************************
-                                    populateAigPointerUnitGF( pNew, topNodeOfAST, vSignal, vAigGFMap );
-                                    
-                                    //*************************************************************************************
-                                    //Step 11c: everything below GF are computed. Now, it is time to create logic for individual 
-                                    // GF nodes (i.e. the OR gate and the latch and the Boolean crown of the AST
-                                    //*************************************************************************************
-                                    Vec_PtrForEachEntry( Aig_Obj_t *, vSignal, pObj, i )
-                                    {
-                                        //*********************************************************
-                                        // Step 11c.1: if the OR+Latch of the particular signal is
-                                        // not already created, create it. It may have already been 
-                                        // created from another property, so check it before creation
-                                        //*********************************************************
-                                        if( Vec_PtrFind( vSignalMemory, pObj ) == -1 )
-                                        {
-                                            liveLatch++;
-
-                                            pDriverImage = pObj;
-                                            pObjShadowLo = Aig_ObjCreatePi( pNew );
-                                            pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-                                            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-
-                                            nRegCount++;
-                                            loCreated++; liCreated++;
-
-                                            Vec_PtrPush( vSignalMemory, pObj );
-                                            Vec_PtrPush( vGFFlopMemory, pObjShadowLo );
-
-                                            #if 1
-                                            #ifdef PROPAGATE_NAMES
-                                                Vec_PtrPush( vecLos, pObjShadowLo );
-                                                //nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                                                //sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
-                                                nodeName = (char *)malloc( 20 );
-                                                sprintf( nodeName, "n%d__%s", Aig_ObjId(pObjShadowLo), "GF_flop" );
-                                                Vec_PtrPush( vecLoNames, nodeName );
-                                            #endif
-                                            #endif
-                                        }
-                                        else
-                                            pObjShadowLo = (Aig_Obj_t *)Vec_PtrEntry( vGFFlopMemory, Vec_PtrFind( vSignalMemory, pObj ) );
-                                                                                
-                                        Vec_VecForEachEntryLevel( ltlNode *, vAigGFMap, pEnrtyGLOBALLY, ii, i )
-                                            setAIGNodePtrOfGloballyNode( pEnrtyGLOBALLY, pObjShadowLo);
-                                            
-
-                                        //#ifdef PROPAGATE_NAMES
-                                        //    Vec_PtrPush( vecLos, pObjShadowLo );
-                                        //    nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-                                        //    sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
-                                        //    Vec_PtrPush( vecLoNames, nodeName );
-                                        //#endif
-                                        
-                                    }
-                                    
-                                    //*********************************************************
-                                    //Step 11c.2: creating the Boolean crown
-                                    //*********************************************************
-                                    buildLogicFromLTLNode( pNew, topNodeOfAST );
-
-                                    //*********************************************************
-                                    //Step 11c.3: creating logic for (looped & ~theta) and patching
-                                    // it with the proper PO
-                                    //Note: if ALLOW_SAFETY_PROPERTIES is defined then the final AND
-                                    //gate is a conjunction of safety & liveness, i.e. SAFETY & (looped => theta)
-                                    //since ABC convention demands a NOT gate at the end, the property logic 
-                                    //becomes !( SAFETY & (looped => theta) ) = !SAFETY + (looped & !theta)
-                                    //*********************************************************
-                                    pObjLive = retriveAIGPointerFromLTLNode( topNodeOfAST );
-                                    pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_Not(pObjLive) );
-                                    #ifdef ALLOW_SAFETY_PROPERTIES
-                                        printf("liveness output is conjoined with safety assertions\n");
-                                        pObjSafetyAndLiveToSafety = Aig_Or( pNew, pObjSafetyGate, pNegatedSafetyConjunction );
-                                        pObjSafetyPropertyOutput = (Aig_Obj_t *)Vec_PtrEntry( vPoForLtlProps, iii );
-                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyAndLiveToSafety );
-                                    #else
-                                        pObjSafetyPropertyOutput = Vec_PtrEntry( vPoForLtlProps, iii );
-                                        Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-                                    #endif
-                                    //refreshing vSignal and vAigGFMap arrays
-                                    Vec_PtrFree( vSignal );
-                                    Vec_VecFree( vAigGFMap );
-                }
-                                
-            #endif
-        }
-#endif
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-    
-    Aig_ManCleanup( pNew );
-    
-    assert( Aig_ManCheck( pNew ) );
-    
-    if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
-    {
-            assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
-            assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
-            //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
-    }
-
-
-    return pNew;
-}
-
-int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
-    Aig_Man_t * pAig, *pAigNew;
-    int c;
-    Vec_Ptr_t * vLive, * vFair, *vAssertSafety, *vAssumeSafety;
-    int directive = -1;
-    char *ltfFormulaString = NULL;
-    int LTL_FLAG = 0, numOfLtlPropOutput;
-    Vec_Ptr_t *ltlBuffer;
-                
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    if( argc == 1 )
-    {
-        assert( directive == -1 );
-        directive = FULL_BIERE_MODE;
-    }
-    else
-    {
-        Extra_UtilGetoptReset();
-        while ( ( c = Extra_UtilGetopt( argc, argv, "1slhf" ) ) != EOF )
-        {
-            switch( c )
-            {
-            case '1': 
-                if( directive == -1 )
-                    directive = FULL_BIERE_ONE_LOOP_MODE;
-                else
-                {
-                    assert( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE || directive == IGNORE_SAFETY_KEEP_LIVENESS_MODE );
-                    if( directive == IGNORE_LIVENESS_KEEP_SAFETY_MODE )
-                        directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                    else
-                        directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 's':
-                if( directive == -1 )
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE;
-                }
-                break;
-            case 'l':
-                if( directive == -1 )
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                else
-                {
-                    if( directive != FULL_BIERE_ONE_LOOP_MODE )
-                        goto usage;
-                    assert(directive == FULL_BIERE_ONE_LOOP_MODE);
-                    directive = IGNORE_LIVENESS_KEEP_SAFETY_MODE;
-                }
-                break;
-            case 'f':
-                //assert( argc >= 3 );
-                //vecLtlFormula = Vec_PtrAlloc( argc - 2 );
-                //if( argc >= 3 )
-                //{
-                //    for( t=3; t<=argc; t++ )
-                //    {
-                //        printf("argv[%d] = %s\n", t-1, argv[t-1]);
-                //        Vec_PtrPush( vecLtlFormula, argv[t-1] );
-                //    }
-                //}
-                //printf("argv[argc] = %s\n", argv[argc-1]);
-                //ltfFormulaString = argv[2];
-                
-                //LTL_FLAG = 1;
-                printf("\nILLEGAL FLAG: aborting....\n");
-                exit(0);
-                break;
-            case 'h':
-                goto usage;
-            default:
-                goto usage;
-            }
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-    if( !Abc_NtkIsStrash( pNtk ) )
-    {
-        printf("The input network was not strashed, strashing....\n");
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkOld = pNtkTemp;
-        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-    else
-    {
-        pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNtkOld = pNtk;
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-        vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-        vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-    }
-
-    if( pAbc->vLTLProperties_global != NULL )
-        ltlBuffer = pAbc->vLTLProperties_global;
-    else
-        ltlBuffer = NULL;
-
-    switch( directive )
-    {
-    case FULL_BIERE_MODE:
-            pAigNew = LivenessToSafetyTransformationWithLTL( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t%d POs - one for safety and %d for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput+1, numOfLtlPropOutput);
-            break;
-        
-    case FULL_BIERE_ONE_LOOP_MODE:
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( FULL_BIERE_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t2 POs - one for safety and one for liveness.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        
-    case IGNORE_LIVENESS_KEEP_SAFETY_MODE:
-            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
-            assert( numOfLtlPropOutput == 0 );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t1 PO - only for safety property; liveness properties are ignored, if any.\n\tno additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created\n\tnon-property POs are suppressed\n");
-            break;
-        
-    case IGNORE_SAFETY_KEEP_LIVENESS_MODE:
-            pAigNew = LivenessToSafetyTransformationWithLTL( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety, &numOfLtlPropOutput, ltlBuffer );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("A new circuit is produced with\n\t%d PO - only for liveness property; safety properties are ignored, if any.\n\tone additional input is added (due to Biere's nondeterminism)\n\tshadow flops are not created if the original circuit is combinational\n\tnon-property POs are suppressed\n", numOfLtlPropOutput);
-            break;
-        
-    case IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE:
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nShadow registers are not created\n");
-            break;
-    }
-
-#if 0
-    if( argc == 1 )
-    {
-        pAigNew = LivenessToSafetyTransformation( FULL_BIERE_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-        if( Aig_ManRegNum(pAigNew) != 0 )
-            printf("New circuit is produced considering all safety, liveness and fairness outputs.\nBiere's logic is created\n");
-    }
-    else 
-    {
-        Extra_UtilGetoptReset();
-        c = Extra_UtilGetopt( argc, argv, "1lsh" );
-        if( c == '1' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformationOneStepLoop( pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-        }
-        else if( c == 'l' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformation( IGNORE_LIVENESS_KEEP_SAFETY_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring liveness outputs!\nOnly safety outputs are kept.\nBiere's logic is not created\n");
-        }
-        else if( c == 's' )
-        {
-            if ( pNtk == NULL )
-            {
-                fprintf( pErr, "Empty network.\n" );
-                return 1;
-            }
-            
-            if( !Abc_NtkIsStrash( pNtk ) )
-            {
-                printf("The input network was not strashed, strashing....\n");
-                pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-                pNtkOld = pNtkTemp;
-                pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            else
-            {
-                pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pNtkOld = pNtk;
-                vLive = populateLivenessVector( pNtk, pAig );
-                vFair = populateFairnessVector( pNtk, pAig );
-                vAssertSafety = populateSafetyAssertionVector( pNtk, pAig );
-                vAssumeSafety = populateSafetyAssumptionVector( pNtk, pAig );
-            }
-            pAigNew = LivenessToSafetyTransformation( IGNORE_SAFETY_KEEP_LIVENESS_MODE, pNtk, pAig, vLive, vFair, vAssertSafety, vAssumeSafety );
-            if( Aig_ManRegNum(pAigNew) != 0 )
-                printf("New circuit is produced ignoring safety outputs!\nOnly liveness and fairness outputs are considered.\nBiere's logic is created\n");
-        }
-        else if( c == 'h' )
-            goto usage;
-        else
-            goto usage;
-    }
-#endif
-    
-#if 0
-    Aig_ManPrintStats( pAigNew );
-    printf("\nDetail statistics*************************************\n");
-    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
-    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
-    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
-    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
-    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
-    printf("\n*******************************************************\n");
-#endif
-
-    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
-    pNtkNew->pName = Aig_UtilStrsav( pAigNew->pName );
-    
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
-    
-    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames, vecLoNames );
-    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
-
-#if 0
-#ifndef DUPLICATE_CKT_DEBUG
-    Saig_ManForEachPi( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
-        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
-
-    Saig_ManForEachLo( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
-#endif    
-#endif
-        
-    return 0;
-
-usage:
-    fprintf( stdout, "usage: l3s [-1lsh]\n" );
-    fprintf( stdout, "\t         performs Armin Biere's live-to-safe transformation\n" );
-    fprintf( stdout, "\t-1 : no shadow logic, presume all loops are self loops\n");
-    fprintf( stdout, "\t-l : ignore liveness and fairness outputs\n");
-    fprintf( stdout, "\t-s : ignore safety assertions and assumptions\n");
-    fprintf( stdout, "\t-h : print command usage\n");
-    return 1;
-}
-
-
-ABC_NAMESPACE_IMPL_END
diff --git a/src/aig/live/liveness_sim.c b/src/aig/live/liveness_sim.c
deleted file mode 100644
index 5e494b87..00000000
--- a/src/aig/live/liveness_sim.c
+++ /dev/null
@@ -1,848 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [liveness_sim.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Liveness property checking.]
-
-  Synopsis    [Main implementation module.]
-
-  Author      [Sayak Ray]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2009.]
-
-  Revision    [$Id: liveness_sim.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include "main.h"
-#include "aig.h"
-#include "saig.h"
-#include <string.h>
-
-ABC_NAMESPACE_IMPL_START
-
-
-#define PROPAGATE_NAMES
-//#define DUPLICATE_CKT_DEBUG
-
-extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-//char *strdup(const char *string);
-
-
-/*******************************************************************
-LAYOUT OF PI VECTOR:
- 
-+------------------------------------------------------------------------------------------------------------------------------------+
-| TRUE ORIGINAL PI (n) | SAVE(PI) (1) | ORIGINAL LO (k) | SAVED(LO) (1) | SHADOW_ORIGINAL LO (k) | LIVENESS LO (l) | FAIRNESS LO (f) |
-+------------------------------------------------------------------------------------------------------------------------------------+
-<------------True PI----------------->|<----------------------------LO--------------------------------------------------------------->
-
-LAYOUT OF PO VECTOR:
-
-+-----------------------------------------------------------------------------------------------------------+
-| SOLE PO (1) | ORIGINAL LI (k) | SAVED LI (1) | SHADOW_ORIGINAL LI (k) | LIVENESS LI (l) | FAIRNESS LI (f) |
-+-----------------------------------------------------------------------------------------------------------+
-<--True PO--->|<--------------------------------------LI---------------------------------------------------->
-
-********************************************************************/
-
-static void printVecPtrOfString( Vec_Ptr_t *vec )
-{
-    int i;
-
-    for( i=0; i< Vec_PtrSize( vec ); i++ )
-    {
-        printf("vec[%d] = %s\n", i, (char *)Vec_PtrEntry(vec, i) );
-    }
-}
-
-static int getPoIndex( Aig_Man_t *pAig, Aig_Obj_t *pPivot )
-{
-    int i;
-    Aig_Obj_t *pObj;
-
-    Saig_ManForEachPo( pAig, pObj, i )
-    {
-        if( pObj == pPivot )
-            return i;
-    }
-    return -1;
-}
-
-static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot )
-{
-    Aig_Obj_t *pObjOld, *pObj;
-    Abc_Obj_t *pNode;
-    int index;
-
-    assert( Saig_ObjIsPi( pAigNew, pObjPivot ) );
-    Aig_ManForEachPi( pAigNew, pObj, index )
-        if( pObj == pObjPivot )
-            break;
-    assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) );
-    if( index == Saig_ManPiNum( pAigNew ) - 1 )
-        return "SAVE_BIERE";
-    else
-    {
-        pObjOld = Aig_ManPi( pAigOld, index );
-        pNode = Abc_NtkPi( pNtkOld, index );
-        assert( pObjOld->pData == pObjPivot );
-        return Abc_ObjName( pNode );
-    }
-}
-
-static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Aig_Obj_t *pObjPivot, Vec_Ptr_t *vLive, Vec_Ptr_t * vFair )
-{
-    Aig_Obj_t *pObjOld, *pObj;
-    Abc_Obj_t *pNode;
-    int index, oldIndex, originalLatchNum = Saig_ManRegNum(pAigOld), strMatch, i;
-    char *dummyStr = (char *)malloc( sizeof(char) * 50 );
-
-    assert( Saig_ObjIsLo( pAigNew, pObjPivot ) );
-    Saig_ManForEachLo( pAigNew, pObj, index )
-        if( pObj == pObjPivot )
-            break;
-    if( index < originalLatchNum )
-    {
-        oldIndex = Saig_ManPiNum( pAigOld ) + index;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
-        pNode = Abc_NtkCi( pNtkOld, oldIndex );
-        assert( pObjOld->pData == pObjPivot );
-        return Abc_ObjName( pNode );
-    }
-    else if( index == originalLatchNum )
-        return "SAVED_LO";
-    else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 )
-    {
-        oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1;
-        pObjOld = Aig_ManPi( pAigOld, oldIndex );
-        pNode = Abc_NtkCi( pNtkOld, oldIndex );
-        sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW");
-        return dummyStr;
-    }
-    else if( index >= 2 * originalLatchNum + 1 && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) )
-    {
-        oldIndex = index - 2 * originalLatchNum - 1;
-        strMatch = 0;
-        Saig_ManForEachPo( pAigOld, pObj, i )
-        {
-            pNode = Abc_NtkPo( pNtkOld, i );
-            if( strstr( Abc_ObjName( pNode ), "assert_fair" ) != NULL )
-            {
-                if( strMatch == oldIndex )
-                {
-                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "LIVENESS");
-                    return dummyStr;
-                }
-                else
-                    strMatch++;
-            }
-        }
-    }
-    else if( index >= 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) && index < 2 * originalLatchNum + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) )
-    {
-        oldIndex = index - 2 * originalLatchNum - 1 - Vec_PtrSize( vLive );
-        strMatch = 0;
-        Saig_ManForEachPo( pAigOld, pObj, i )
-        {
-            pNode = Abc_NtkPo( pNtkOld, i );
-            if( strstr( Abc_ObjName( pNode ), "assume_fair" ) != NULL )
-            {
-                if( strMatch == oldIndex )
-                {
-                    sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "FAIRNESS");
-                    return dummyStr;
-                }
-                else
-                    strMatch++;
-            }
-        }
-    }
-    else
-        return "UNKNOWN";
-}
-
-extern Vec_Ptr_t *vecPis, *vecPiNames;
-extern Vec_Ptr_t *vecLos, *vecLoNames;
-
-
-static int Aig_ManPiCleanupBiere( Aig_Man_t * p )
-{
-    int k = 0, nPisOld = Aig_ManPiNum(p);
-    
-    p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
-    if ( Aig_ManRegNum(p) )
-        p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
-    
-    return nPisOld - Aig_ManPiNum(p);
-}
-
-
-static int Aig_ManPoCleanupBiere( Aig_Man_t * p )
-{
-    int k = 0, nPosOld = Aig_ManPoNum(p);
-
-    p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
-    if ( Aig_ManRegNum(p) )
-        p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
-    return nPosOld - Aig_ManPoNum(p);
-}
-
-static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
-{
-    Aig_Man_t * pNew;
-    int i, nRegCount;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObjSavedLo, *pObjSavedLi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSaveOrSaved, *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjShadowLo, *pObjShadowLi, *pObjShadowLiDriver;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
-    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage;
-    char *nodeName;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0, liveLatch = 0, fairLatch = 0;
-    
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-#ifdef DUPLICATE_CKT_DEBUG
-    printf("\nCode is compiled in DEBUG mode, the input-output behavior will be the same as the original circuit\n");
-    printf("Press any key to continue...");
-    scanf("%c", &c);
-#endif
-
-    //****************************************************************
-    // Step1: create the new manager
-    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-    // nodes, but this selection is arbitrary - need to be justified
-    //****************************************************************
-    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( "live2safe" );
-    pNew->pSpec = NULL;
-    
-    //****************************************************************
-    // Step 2: map constant nodes
-    //****************************************************************
-    pObj = Aig_ManConst1( p );
-    pObj->pData = Aig_ManConst1( pNew );
-
-    //****************************************************************
-    // Step 3: create true PIs
-    //****************************************************************
-    Saig_ManForEachPi( p, pObj, i )
-    {
-        piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecPis, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 4: create the special Pi corresponding to SAVE
-    //****************************************************************
-#ifndef DUPLICATE_CKT_DEBUG
-    pObjSavePi = Aig_ObjCreatePi( pNew );
-    nodeName = Aig_UtilStrsav("SAVE_BIERE"),
-    Vec_PtrPush( vecPiNames, nodeName );
-#endif
-        
-    //****************************************************************
-    // Step 5: create register outputs
-    //****************************************************************
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecLos, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 6: create "saved" register output
-    //****************************************************************
-#ifndef DUPLICATE_CKT_DEBUG
-    loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
-    Vec_PtrPush( vecLos, pObjSavedLo );
-    nodeName = Aig_UtilStrsav("SAVED_LO");
-    Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-    //****************************************************************
-    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-    //****************************************************************
-#ifndef DUPLICATE_CKT_DEBUG
-    pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-    //pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-#endif
-
-    //********************************************************************
-    // Step 8: create internal nodes
-    //********************************************************************
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    }
-
-    //********************************************************************
-    // Step 9: create the safety property output gate
-    // create the safety property output gate, this will be the sole true PO 
-    // of the whole circuit, discuss with Sat/Alan for an alternative implementation
-    //********************************************************************
-#ifndef DUPLICATE_CKT_DEBUG
-    pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-#endif
-
-    //********************************************************************
-    // DEBUG: To recreate the same circuit, at least from the input and output
-    // behavior, we need to copy the original PO
-    //********************************************************************
-#ifdef DUPLICATE_CKT_DEBUG
-    Saig_ManForEachPo( p, pObj, i )
-    {
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-    }
-#endif
-
-    // create register inputs for the original registers
-    nRegCount = 0;
-    
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-        nRegCount++;
-        liCopied++;
-    }
-
-    // create register input corresponding to the register "saved"
-#ifndef DUPLICATE_CKT_DEBUG
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-    nRegCount++;
-    liCreated++;
-
-    pObjAndAcc = NULL;
-
-    // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator 
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-#ifdef PROPAGATE_NAMES
-        Vec_PtrPush( vecLos, pObjShadowLo );
-        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ) ) + 10 );
-        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "SHADOW" );
-        Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-        pObjShadowLiDriver = Aig_Mux( pNew, pObjSavePi, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-        pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-        nRegCount++;
-        loCreated++; liCreated++;
-        
-        pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData, pObjShadowLo );
-        pObjXnor = Aig_Not( pObjXor );
-        if( pObjAndAcc == NULL )
-            pObjAndAcc = pObjXnor;
-        else
-        {
-            pObjAndAccDummy = pObjAndAcc;
-            pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
-        }
-    }
-
-    // create the AND gate whose output will be the signal "looped"
-    pObjSavedLoAndEquality = Aig_And( pNew, pObjSavedLo, pObjAndAcc );
-    
-    // create the master AND gate and corresponding AND and OR logic for the liveness properties
-    pObjAndAcc = NULL;
-    if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
-        printf("\nCircuit without any liveness property\n");
-    else
-    {
-        Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
-        {
-            //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
-            //Aig_ObjPrint( pNew, pObj );
-            liveLatch++;
-            pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-#ifdef PROPAGATE_NAMES
-        Vec_PtrPush( vecLos, pObjShadowLo );
-        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "LIVENESS" );
-        Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-            pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
-                                                Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-            nRegCount++;
-            loCreated++; liCreated++;
-            
-            if( pObjAndAcc == NULL )
-                pObjAndAcc = pObjShadowLo;
-            else
-            {
-                pObjAndAccDummy = pObjAndAcc;
-                pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAccDummy );
-            }
-        }
-    }
-
-    if( pObjAndAcc != NULL )
-        pObjLive = pObjAndAcc;
-    else
-        pObjLive = Aig_ManConst1( pNew );
-    
-    // create the master AND gate and corresponding AND and OR logic for the fairness properties
-    pObjAndAcc = NULL;
-    if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
-        printf("\nCircuit without any fairness property\n");
-    else
-    {
-        Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
-        {
-            fairLatch++;
-            //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) );
-            pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            pObjShadowLo = Aig_ObjCreatePi( pNew );
-
-#ifdef PROPAGATE_NAMES
-        Vec_PtrPush( vecLos, pObjShadowLo );
-        nodeName = (char *)malloc( strlen( Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ) ) + 12 );
-        sprintf( nodeName, "%s__%s", Abc_ObjName( Abc_NtkPo( pNtk, getPoIndex( p, pObj ) ) ), "FAIRNESS" );
-        Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-            pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), 
-                                    Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) );
-            pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver );
-            nRegCount++;
-            loCreated++; liCreated++;
-            
-            if( pObjAndAcc == NULL )
-                pObjAndAcc = pObjShadowLo;
-            else
-            {
-                pObjAndAccDummy = pObjAndAcc;
-                pObjAndAcc = Aig_And( pNew, pObjShadowLo, pObjAndAccDummy );
-            }
-        }
-    }
-
-    if( pObjAndAcc != NULL )
-        pObjFair = pObjAndAcc;
-    else
-        pObjFair = Aig_ManConst1( pNew );
-    
-    //pObjSafetyGate = Aig_Exor( pNew, Aig_Not(Aig_ManConst1( pNew )), Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) ) );
-    pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
-    
-    Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-#endif
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-    
-    Aig_ManCleanup( pNew );
-    assert( Aig_ManCheck( pNew ) );
-    
-#ifndef DUPLICATE_CKT_DEBUG
-    assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
-    assert( Saig_ManPoNum( pNew ) == 1 );
-    assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
-    assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
-#endif
-
-    return pNew;
-}
-
-
-static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair )
-{
-    Aig_Man_t * pNew;
-    int i, nRegCount;
-    Aig_Obj_t * pObjSavePi;
-    Aig_Obj_t *pObj, *pMatch;
-    Aig_Obj_t *pObjSavedLoAndEquality;
-    Aig_Obj_t *pObjXor, *pObjXnor, *pObjAndAcc, *pObjAndAccDummy;
-    Aig_Obj_t *pObjLive, *pObjFair, *pObjSafetyGate;
-    Aig_Obj_t *pObjSafetyPropertyOutput;
-    Aig_Obj_t *pDriverImage;
-    Aig_Obj_t *pObjCorrespondingLi;
-
-
-    char *nodeName;
-    int piCopied = 0, liCopied = 0, loCopied = 0, liCreated = 0, loCreated = 0, piVecIndex = 0;
-    
-    vecPis = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-    vecPiNames = Vec_PtrAlloc( Saig_ManPiNum( p ) + 1);
-
-    vecLos = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-    vecLoNames = Vec_PtrAlloc( Saig_ManRegNum( p )*2 + 1 + Vec_PtrSize( vLive ) + Vec_PtrSize( vFair ) );
-
-    //****************************************************************
-    // Step1: create the new manager
-    // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
-    // nodes, but this selection is arbitrary - need to be justified
-    //****************************************************************
-    pNew = Aig_ManStart( 2 * Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( "live2safe" );
-    pNew->pSpec = NULL;
-    
-    //****************************************************************
-    // Step 2: map constant nodes
-    //****************************************************************
-    pObj = Aig_ManConst1( p );
-    pObj->pData = Aig_ManConst1( pNew );
-
-    //****************************************************************
-    // Step 3: create true PIs
-    //****************************************************************
-    Saig_ManForEachPi( p, pObj, i )
-    {
-        piCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecPis, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) ));
-        Vec_PtrPush( vecPiNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 4: create the special Pi corresponding to SAVE
-    //****************************************************************
-    pObjSavePi = Aig_ObjCreatePi( pNew );
-    nodeName = "SAVE_BIERE",
-    Vec_PtrPush( vecPiNames, nodeName );
-        
-    //****************************************************************
-    // Step 5: create register outputs
-    //****************************************************************
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        loCopied++;
-        pObj->pData = Aig_ObjCreatePi(pNew);
-        Vec_PtrPush( vecLos, pObj->pData );
-        nodeName = Aig_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ));
-        Vec_PtrPush( vecLoNames, nodeName );
-    }
-
-    //****************************************************************
-    // Step 6: create "saved" register output
-    //****************************************************************
-
-#if 0
-    loCreated++;
-    pObjSavedLo = Aig_ObjCreatePi( pNew );
-    Vec_PtrPush( vecLos, pObjSavedLo );
-    nodeName = "SAVED_LO";
-    Vec_PtrPush( vecLoNames, nodeName );
-#endif
-
-    //****************************************************************
-    // Step 7: create the OR gate and the AND gate directly fed by "SAVE" Pi
-    //****************************************************************
-#if 0
-    pObjSaveOrSaved = Aig_Or( pNew, pObjSavePi, pObjSavedLo );
-    pObjSaveAndNotSaved = Aig_And( pNew, pObjSavePi, Aig_Not(pObjSavedLo) );
-#endif
-
-    //********************************************************************
-    // Step 8: create internal nodes
-    //********************************************************************
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    }
-
-    //********************************************************************
-    // Step 9: create the safety property output gate
-    // create the safety property output gate, this will be the sole true PO 
-    // of the whole circuit, discuss with Sat/Alan for an alternative implementation
-    //********************************************************************
-
-    pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData );
-
-    // create register inputs for the original registers
-    nRegCount = 0;
-    
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pMatch = Saig_ObjLoToLi( p, pObj );
-        //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) );
-        Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) );
-        nRegCount++;
-        liCopied++;
-    }
-
-#if 0
-    // create register input corresponding to the register "saved"
-    pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved );
-    nRegCount++;
-    liCreated++;
-#endif
-
-    pObjAndAcc = NULL;
-
-    //****************************************************************************************************
-    //For detection of loop of length 1 we do not need any shadow register, we only need equality detector
-    //between Lo_j and Li_j and then a cascade of AND gates
-    //****************************************************************************************************
-
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        pObjCorrespondingLi = Saig_ObjLoToLi( p, pObj );
-        
-        pObjXor = Aig_Exor( pNew, (Aig_Obj_t *)pObj->pData,  Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0( pObjCorrespondingLi )->pData, Aig_ObjFaninC0( pObjCorrespondingLi ) ) );
-        pObjXnor = Aig_Not( pObjXor );
-        
-        if( pObjAndAcc == NULL )
-            pObjAndAcc = pObjXnor;
-        else
-        {
-            pObjAndAccDummy = pObjAndAcc;
-            pObjAndAcc = Aig_And( pNew, pObjXnor, pObjAndAccDummy );
-        }
-    }
-
-    // create the AND gate whose output will be the signal "looped"
-    pObjSavedLoAndEquality = Aig_And( pNew, pObjSavePi, pObjAndAcc );
-    
-    // create the master AND gate and corresponding AND and OR logic for the liveness properties
-    pObjAndAcc = NULL;
-    if( vLive == NULL || Vec_PtrSize( vLive ) == 0 )
-        printf("\nCircuit without any liveness property\n");
-    else
-    {
-        Vec_PtrForEachEntry( Aig_Obj_t *, vLive, pObj, i )
-        {
-            pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            if( pObjAndAcc == NULL )
-                pObjAndAcc = pDriverImage;
-            else
-            {
-                pObjAndAccDummy = pObjAndAcc;
-                pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
-            }
-        }
-    }
-
-    if( pObjAndAcc != NULL )
-        pObjLive = pObjAndAcc;
-    else
-        pObjLive = Aig_ManConst1( pNew );
-    
-    // create the master AND gate and corresponding AND and OR logic for the fairness properties
-    pObjAndAcc = NULL;
-    if( vFair == NULL || Vec_PtrSize( vFair ) == 0 )
-        printf("\nCircuit without any fairness property\n");
-    else
-    {
-        Vec_PtrForEachEntry( Aig_Obj_t *, vFair, pObj, i )
-        {
-            pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-            if( pObjAndAcc == NULL )
-                pObjAndAcc = pDriverImage;
-            else
-            {
-                pObjAndAccDummy = pObjAndAcc;
-                pObjAndAcc = Aig_And( pNew, pDriverImage, pObjAndAccDummy );
-            }
-        }
-    }
-
-    if( pObjAndAcc != NULL )
-        pObjFair = pObjAndAcc;
-    else
-        pObjFair = Aig_ManConst1( pNew );
-    
-    pObjSafetyGate = Aig_And( pNew, pObjSavedLoAndEquality, Aig_And( pNew, pObjFair, Aig_Not( pObjLive ) ) );
-    
-    Aig_ObjPatchFanin0( pNew, pObjSafetyPropertyOutput, pObjSafetyGate );
-
-    Aig_ManSetRegNum( pNew, nRegCount );
-
-    printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs );
-
-    Aig_ManPiCleanupBiere( pNew );
-    Aig_ManPoCleanupBiere( pNew );
-
-    Aig_ManCleanup( pNew );
-    
-    assert( Aig_ManCheck( pNew ) );
-    
-    return pNew;
-}
-
-
-
-static Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, liveCounter = 0;
-    Vec_Ptr_t * vLive;
-
-    vLive = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL )
-        {
-            Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) );
-            liveCounter++;
-        }
-    printf("\nNumber of liveness property found = %d\n", liveCounter);
-    return vLive;
-}
-
-static Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
-{
-    Abc_Obj_t * pNode;
-    int i, fairCounter = 0;
-    Vec_Ptr_t * vFair;
-
-    vFair = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL )
-        {
-            Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) );
-            fairCounter++;
-        }
-    printf("\nNumber of fairness property found = %d\n", fairCounter);
-    return vFair;
-}
-
-static void updateNewNetworkNameManager( Abc_Ntk_t *pNtk, Aig_Man_t *pAig, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vLoNames )
-{
-    Aig_Obj_t *pObj;
-    int i, ntkObjId;
-
-    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum( pNtk ) );
-
-    Saig_ManForEachPi( pAig, pObj, i )
-    {
-        ntkObjId = Abc_NtkCi( pNtk, i )->Id;
-        //printf("Pi %d, Saved Name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vPiNames, i), NULL ), ntkObjId);  
-        Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vPiNames, i), NULL );
-    }
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-        ntkObjId = Abc_NtkCi( pNtk, Saig_ManPiNum( pAig ) + i )->Id;
-        //printf("Lo %d, Saved name = %s, id = %d\n", i, Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), Vec_PtrEntry(vLoNames, i), NULL ), ntkObjId);  
-        Nm_ManStoreIdName( pNtk->pManName, ntkObjId, Aig_ObjType(pObj), (char *)Vec_PtrEntry(vLoNames, i), NULL );
-    }
-}
-
-
-int Abc_CommandAbcLivenessToSafetySim( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkTemp, *pNtkNew, *pNtkOld;
-    Aig_Man_t * pAig, *pAigNew;
-    int c;
-    Vec_Ptr_t * vLive, * vFair;
-                
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if( !Abc_NtkIsStrash( pNtk ) )
-    {
-        printf("\nThe input network was not strashed, strashing....\n");
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkOld = pNtkTemp;
-        pAig = Abc_NtkToDar( pNtkTemp, 0, 1 );
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-    }
-    else
-    {
-        pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNtkOld = pNtk;
-        vLive = populateLivenessVector( pNtk, pAig );
-        vFair = populateFairnessVector( pNtk, pAig );
-    }
-
-#if 0
-    Aig_ManPrintStats( pAig );
-    printf("\nDetail statistics*************************************\n");
-    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAig ));
-    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAig ));
-    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAig ) - Saig_ManPiNum( pAig ));
-    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAig ) - Saig_ManPoNum( pAig ));
-    printf("Numer of registers = %d\n", Saig_ManRegNum( pAig ) );
-    printf("\n*******************************************************\n");
-#endif
-
-    c = Extra_UtilGetopt( argc, argv, "1" );
-    if( c == '1' )
-        pAigNew = LivenessToSafetyTransformationOneStepLoopSim( pNtk, pAig, vLive, vFair );
-    else
-        pAigNew = LivenessToSafetyTransformationSim( pNtk, pAig, vLive, vFair );
-    
-#if 0
-    Aig_ManPrintStats( pAigNew );
-    printf("\nDetail statistics*************************************\n");
-    printf("Number of true primary inputs = %d\n", Saig_ManPiNum( pAigNew ));
-    printf("Number of true primary outputs = %d\n", Saig_ManPoNum( pAigNew ));
-    printf("Number of true latch outputs = %d\n", Saig_ManCiNum( pAigNew ) - Saig_ManPiNum( pAigNew ));
-    printf("Number of true latch inputs = %d\n", Saig_ManCoNum( pAigNew ) - Saig_ManPoNum( pAigNew ));
-    printf("Numer of registers = %d\n", Saig_ManRegNum( pAigNew ) );
-    printf("\n*******************************************************\n");
-#endif
-
-    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
-
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" );
-    
-    updateNewNetworkNameManager( pNtkNew, pAigNew, vecPiNames,vecLoNames );
-    Abc_FrameSetCurrentNetwork( pAbc, pNtkNew );
-
-    //Saig_ManForEachPi( pAigNew, pObj, i )
-    //    printf("Name of %d-th Pi = %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) );
-
-    //Saig_ManForEachLo( pAigNew, pObj, i )
-    //    printf("Name of %d-th Lo = %s\n", i, retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) );
-
-    //printVecPtrOfString( vecPiNames );
-    //printVecPtrOfString( vecLoNames );
-
-#if 0
-#ifndef DUPLICATE_CKT_DEBUG
-    Saig_ManForEachPi( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecPiNames, i), retrieveTruePiName( pNtk, pAig, pAigNew, pObj ) ) == 0 );
-        //printf("Name of %d-th Pi = %s, %s\n", i, retrieveTruePiName( pNtk, pAig, pAigNew, pObj ), (char *)Vec_PtrEntry(vecPiNames, i) );
-
-    Saig_ManForEachLo( pAigNew, pObj, i )
-        assert( strcmp( (char *)Vec_PtrEntry(vecLoNames, i), retrieveLOName( pNtk, pAig, pAigNew, pObj, vLive, vFair ) ) == 0 );
-#endif    
-#endif
-        
-    return 0;
-
-}
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/live/ltl_parser.c b/src/aig/live/ltl_parser.c
deleted file mode 100644
index de113ba7..00000000
--- a/src/aig/live/ltl_parser.c
+++ /dev/null
@@ -1,839 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ltl_parser.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Liveness property checking.]
-
-  Synopsis    [LTL checker.]
-
-  Author      [Sayak Ray]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 1, 2009.]
-
-  Revision    [$Id: ltl_parser.c,v 1.00 2009/01/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <string.h>
-#include <assert.h>
-#include <stdlib.h>
-#include "aig.h"
-#include "abc.h"
-#include "mainInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-enum ltlToken { AND, OR, NOT, IMPLY, GLOBALLY, EVENTUALLY, NEXT, UNTIL, BOOL };
-enum ltlGrammerToken { OPERAND, LTL, BINOP, UOP };
-typedef enum ltlToken tokenType;
-typedef enum ltlGrammerToken ltlGrammerTokenType;
-
-struct ltlNode_t
-{
-    tokenType type;
-    char *name;
-    Aig_Obj_t *pObj;
-    struct ltlNode_t *left;
-    struct ltlNode_t *right;
-};
-
-typedef struct ltlNode_t ltlNode;
-
-ltlNode *generateTypedNode( tokenType new_type )
-//void generateTypedNode( ltlNode *new_node, tokenType new_type )
-{
-    ltlNode *new_node;
-
-    new_node = (ltlNode *)malloc( sizeof(ltlNode) );
-    if( new_node )
-    {
-        new_node->type = new_type;
-        new_node->pObj = NULL;
-        new_node->name = NULL;
-        new_node->left = NULL;
-        new_node->right = NULL;
-    }
-
-    return new_node;
-}
-
-Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAig, ltlNode *pLtlNode );
-
-static inline int isNotVarNameSymbol( char c )
-{
-    return ( c == ' ' || c == '\t' || c == '\n' || c == ':' || c == '\0' );
-}
-
-void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk )
-{
-    char *pLtlFormula, *tempFormula;
-    int i;
-
-    if( pAbc->vLTLProperties_global != NULL )
-    {
-//        printf("Deleting exisitng LTL database from the frame\n");
-        Vec_PtrFree( pAbc->vLTLProperties_global );
-        pAbc->vLTLProperties_global = NULL;
-    }
-    pAbc->vLTLProperties_global = Vec_PtrAlloc(Vec_PtrSize(pNtk->vLtlProperties));
-    Vec_PtrForEachEntry( char *, pNtk->vLtlProperties, pLtlFormula, i )
-    {
-        tempFormula = (char *)malloc( sizeof(char)*(strlen(pLtlFormula)+1) );
-        sprintf( tempFormula, "%s", pLtlFormula );
-        Vec_PtrPush( pAbc->vLTLProperties_global, tempFormula );
-    }
-}
-
-char *getVarName( char *suffixFormula, int startLoc, int *endLocation )
-{
-    int i = startLoc, length;
-    char *name;
-
-    if( isNotVarNameSymbol( suffixFormula[startLoc] ) )
-        return NULL;
-
-    while( !isNotVarNameSymbol( suffixFormula[i] ) )
-        i++;
-    *endLocation = i;
-    length = i - startLoc;
-    name = (char *)malloc( sizeof(char) * (length + 1));
-    for( i=0; i<length; i++ )
-        name[i] = suffixFormula[i+startLoc];
-    name[i] = '\0';
-
-    return name;
-}
-
-
-int startOfSuffixString = 0;
-
-int isUnexpectedEOS( char *formula, int index )
-{
-    assert( formula );
-    if( index >= (int)strlen( formula ) )
-    {
-        printf("\nInvalid LTL formula: unexpected end of string..." );
-        return 1;
-    }
-    return 0;
-}
-
-int isTemporalOperator( char *formula, int index )
-{
-    if( !(isUnexpectedEOS( formula, index ) || formula[ index ] == 'G' || formula[ index ] == 'F' || formula[ index ] == 'U' || formula[ index ] == 'X') )
-    {
-        printf("\nInvalid LTL formula: expecting temporal operator at the position %d....\n", index);
-        return 0;
-    }
-    return 1;
-}
-
-ltlNode *readLtlFormula( char *formula )
-{
-    char ch;
-    char *varName;
-    int formulaLength, rememberEnd;
-    int i = startOfSuffixString;
-    ltlNode *curr_node, *temp_node_left, *temp_node_right;
-    char prevChar;
-    
-    formulaLength = strlen( formula );
-    if( isUnexpectedEOS( formula, startOfSuffixString ) )
-    {
-        printf("\nFAULTING POINT: formula = %s\nstartOfSuffixString = %d, formula[%d] = %c\n\n", formula, startOfSuffixString, startOfSuffixString - 1, formula[startOfSuffixString-1]);
-        return NULL;
-    }
-            
-    while( i < formulaLength )
-    {
-        ch = formula[i];
-
-        switch(ch){
-            case ' ':
-            case '\n':
-            case '\r':
-            case '\t':
-            case '\v':
-            case '\f':
-                        i++;
-                        startOfSuffixString = i;
-                        break;
-            case ':':
-                        i++;
-                        if( !isTemporalOperator( formula, i ) )
-                            return NULL;
-                        startOfSuffixString = i;
-                        break;
-            case 'G':
-                        prevChar = formula[i-1];
-                        if( prevChar == ':' ) //i.e. 'G' is a temporal operator
-                        {
-                            i++;
-                            startOfSuffixString = i;
-                            temp_node_left = readLtlFormula( formula );
-                            if( temp_node_left == NULL )
-                                return NULL;
-                            else
-                            {
-                                curr_node = generateTypedNode(GLOBALLY);
-                                curr_node->left = temp_node_left;
-                                return curr_node;
-                            }
-                        }
-                        else    //i.e. 'G' must be starting a variable name
-                        {
-                            varName = getVarName( formula, i, &rememberEnd );
-                            if( !varName )
-                            {
-                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
-                                return NULL;
-                            }
-                            curr_node = generateTypedNode(BOOL);
-                            curr_node->name = varName;
-                            i = rememberEnd;
-                            startOfSuffixString = i;
-                            return curr_node;
-                        }
-            case 'F':
-                        prevChar = formula[i-1];
-                        if( prevChar == ':' ) //i.e. 'F' is a temporal operator
-                        {
-                            i++;
-                            startOfSuffixString = i;
-                            temp_node_left = readLtlFormula( formula );
-                            if( temp_node_left == NULL )
-                                return NULL;
-                            else
-                            {
-                                curr_node = generateTypedNode(EVENTUALLY);
-                                curr_node->left = temp_node_left;
-                                return curr_node;
-                            }
-                        }
-                        else //i.e. 'F' must be starting a variable name
-                        {
-                            varName = getVarName( formula, i, &rememberEnd );
-                            if( !varName )
-                            {
-                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
-                                return NULL;
-                            }
-                            curr_node = generateTypedNode(BOOL);
-                            curr_node->name = varName;
-                            i = rememberEnd;
-                            startOfSuffixString = i;
-                            return curr_node;
-                        }    
-            case 'X':
-                        prevChar = formula[i-1];
-                        if( prevChar == ':' ) //i.e. 'X' is a temporal operator
-                        {
-                            i++;
-                            startOfSuffixString = i;
-                            temp_node_left = readLtlFormula( formula );
-                            if( temp_node_left == NULL )
-                                return NULL;
-                            else
-                            {
-                                curr_node = generateTypedNode(NEXT);
-                                curr_node->left = temp_node_left;
-                                return curr_node;
-                            }
-                        }
-                        else //i.e. 'X' must be starting a variable name
-                        {
-                            varName = getVarName( formula, i, &rememberEnd );
-                            if( !varName )
-                            {
-                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
-                                return NULL;
-                            }
-                            curr_node = generateTypedNode(BOOL);
-                            curr_node->name = varName;
-                            i = rememberEnd;
-                            startOfSuffixString = i;
-                            return curr_node;
-                        }    
-            case 'U':
-                        prevChar = formula[i-1];
-                        if( prevChar == ':' ) //i.e. 'X' is a temporal operator
-                        {
-                            i++;
-                            startOfSuffixString = i;
-                            temp_node_left = readLtlFormula( formula );
-                            if( temp_node_left == NULL )
-                                return NULL;
-                            temp_node_right = readLtlFormula( formula );
-                            if( temp_node_right == NULL )
-                            {
-                                //need to do memory management: if right subtree is NULL then left
-                                //subtree must be freed.
-                                return NULL;
-                            }
-                            curr_node = generateTypedNode(UNTIL);
-                            curr_node->left = temp_node_left;
-                            curr_node->right = temp_node_right;
-                            return curr_node;
-                        }
-                        else //i.e. 'U' must be starting a variable name
-                        {
-                            varName = getVarName( formula, i, &rememberEnd );
-                            if( !varName )
-                            {
-                                printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
-                                return NULL;
-                            }
-                            curr_node = generateTypedNode(BOOL);
-                            curr_node->name = varName;
-                            i = rememberEnd;
-                            startOfSuffixString = i;
-                            return curr_node;
-                        }    
-            case '+':
-                        i++;
-                        startOfSuffixString = i;
-                        temp_node_left = readLtlFormula( formula );
-                        if( temp_node_left == NULL )
-                            return NULL;
-                        temp_node_right = readLtlFormula( formula );
-                        if( temp_node_right == NULL )
-                        {
-                            //need to do memory management: if right subtree is NULL then left
-                            //subtree must be freed.
-                            return NULL;
-                        }
-                        curr_node = generateTypedNode(OR);
-                        curr_node->left = temp_node_left;
-                        curr_node->right = temp_node_right;
-                        return curr_node;
-            case '&':
-                        i++;
-                        startOfSuffixString = i;
-                        temp_node_left = readLtlFormula( formula );
-                        if( temp_node_left == NULL )
-                            return NULL;
-                        temp_node_right = readLtlFormula( formula );
-                        if( temp_node_right == NULL )
-                        {
-                            //need to do memory management: if right subtree is NULL then left
-                            //subtree must be freed.
-                            return NULL;
-                        }
-                        curr_node = generateTypedNode(AND);
-                        curr_node->left = temp_node_left;
-                        curr_node->right = temp_node_right;
-                        return curr_node;
-            case '!':
-                        i++;
-                        startOfSuffixString = i;
-                        temp_node_left = readLtlFormula( formula );
-                        if( temp_node_left == NULL )
-                            return NULL;
-                        else
-                        {
-                            curr_node = generateTypedNode(NOT);
-                            curr_node->left = temp_node_left;
-                            return curr_node;
-                        }
-            default:
-                varName = getVarName( formula, i, &rememberEnd );
-                if( !varName )
-                {
-                    printf("\nInvalid LTL formula: expecting valid variable name token...aborting" );
-                    return NULL;
-                }
-                curr_node = generateTypedNode(BOOL);
-                curr_node->name = varName;
-                i = rememberEnd;
-                startOfSuffixString = i;
-                return curr_node;
-        }
-    }
-    return NULL;
-}
-
-void resetGlobalVar()
-{
-    startOfSuffixString = 0;
-}
-
-ltlNode *parseFormulaCreateAST( char *inputFormula )
-{
-    ltlNode *temp;
-
-    temp = readLtlFormula( inputFormula );
-    //if( temp == NULL )
-    //    printf("\nAST creation failed for formula %s", inputFormula );
-    resetGlobalVar();
-    return temp;
-}
-
-void traverseAbstractSyntaxTree( ltlNode *node )
-{
-    switch(node->type){
-        case( AND ):
-            printf("& ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            traverseAbstractSyntaxTree( node->right );
-            return;
-        case( OR ):
-            printf("+ ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            traverseAbstractSyntaxTree( node->right );
-            return;
-        case( NOT ):
-            printf("~ ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            assert( node->right == NULL );
-            return;
-        case( GLOBALLY ):
-            printf("G ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            assert( node->right == NULL );
-            return;
-        case( EVENTUALLY ):
-            printf("F ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            assert( node->right == NULL );
-            return;
-        case( NEXT ):
-            printf("X ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            assert( node->right == NULL );
-            return;
-        case( UNTIL ):
-            printf("U ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree( node->left );
-            traverseAbstractSyntaxTree( node->right );
-            return;
-        case( BOOL ):
-            printf("%s ", node->name);
-            assert( node->left == NULL );
-            assert( node->right == NULL );
-            return;
-        default:
-            printf("\nUnsupported token type: Exiting execution\n");
-            exit(0);
-    }
-}
-
-void traverseAbstractSyntaxTree_postFix( ltlNode *node )
-{
-    switch(node->type){
-        case( AND ):
-            printf("( ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            printf("& ");
-            traverseAbstractSyntaxTree_postFix( node->right );
-            printf(") ");
-            return;
-        case( OR ):
-            printf("( ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            printf("+ ");
-            traverseAbstractSyntaxTree_postFix( node->right );
-            printf(") ");
-            return;
-        case( NOT ):
-            printf("~ ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            assert( node->right == NULL );
-            return;
-        case( GLOBALLY ):
-            printf("G ");
-            //printf("( ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            assert( node->right == NULL );
-            //printf(") ");
-            return;
-        case( EVENTUALLY ):
-            printf("F ");
-            //printf("( ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            assert( node->right == NULL );
-            //printf(") ");
-            return;
-        case( NEXT ):
-            printf("X ");
-            assert( node->left != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            assert( node->right == NULL );
-            return;
-        case( UNTIL ):
-            printf("( ");
-            assert( node->left != NULL );
-            assert( node->right != NULL );
-            traverseAbstractSyntaxTree_postFix( node->left );
-            printf("U ");
-            traverseAbstractSyntaxTree_postFix( node->right );
-            printf(") ");
-            return;
-        case( BOOL ):
-            printf("%s ", node->name);
-            assert( node->left == NULL );
-            assert( node->right == NULL );
-            return;
-        default:
-            printf("\nUnsupported token type: Exiting execution\n");
-            exit(0);
-    }
-}
-
-void populateAigPointerUnitGF( Aig_Man_t *pAigNew, ltlNode *topASTNode, Vec_Ptr_t *vSignal, Vec_Vec_t *vAigGFMap )
-{
-    ltlNode *nextNode, *nextToNextNode;
-    int serialNumSignal;
-
-    switch( topASTNode->type ){
-        case AND:
-        case OR:
-        case IMPLY:
-            populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
-            populateAigPointerUnitGF( pAigNew, topASTNode->right, vSignal, vAigGFMap );
-            return;
-        case NOT:
-            populateAigPointerUnitGF( pAigNew, topASTNode->left, vSignal, vAigGFMap );
-            return;
-        case GLOBALLY:
-            nextNode = topASTNode->left;
-            assert( nextNode->type = EVENTUALLY );
-            nextToNextNode = nextNode->left;
-            if( nextToNextNode->type == BOOL )
-            {
-                assert( nextToNextNode->pObj );
-                serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
-                if( serialNumSignal == -1 )
-                {                    
-                    Vec_PtrPush( vSignal, nextToNextNode->pObj );
-                    serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
-                }
-                //Vec_PtrPush( vGLOBALLY, topASTNode );
-                Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
-            }
-            else
-            {
-                assert( nextToNextNode->pObj == NULL );
-                buildLogicFromLTLNode_combinationalOnly( pAigNew, nextToNextNode );
-                serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
-                if( serialNumSignal == -1 )
-                {
-                    Vec_PtrPush( vSignal, nextToNextNode->pObj );
-                    serialNumSignal = Vec_PtrFind( vSignal, nextToNextNode->pObj );
-                }
-                //Vec_PtrPush( vGLOBALLY, topASTNode );
-                Vec_VecPush( vAigGFMap, serialNumSignal, topASTNode );
-            }
-            return;
-        case BOOL:
-            return;
-        default:
-            printf("\nINVALID situation: aborting...\n");
-            exit(0);
-    }
-}
-
-Aig_Obj_t *buildLogicFromLTLNode_combinationalOnly( Aig_Man_t *pAigNew, ltlNode *pLtlNode )
-{
-    Aig_Obj_t *leftAigObj, *rightAigObj;
-
-    if( pLtlNode->pObj != NULL )
-        return pLtlNode->pObj;
-    else
-    {
-        assert( pLtlNode->type != BOOL );
-        switch( pLtlNode->type ){
-            case AND:
-                assert( pLtlNode->left ); assert( pLtlNode->right );
-                leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
-                rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
-                assert( leftAigObj ); assert( rightAigObj );
-                pLtlNode->pObj = Aig_And( pAigNew, leftAigObj, rightAigObj );
-                return pLtlNode->pObj;
-            case OR:
-                assert( pLtlNode->left ); assert( pLtlNode->right );
-                leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
-                rightAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->right );
-                assert( leftAigObj ); assert( rightAigObj );
-                pLtlNode->pObj = Aig_Or( pAigNew, leftAigObj, rightAigObj );
-                return pLtlNode->pObj;
-            case NOT:
-                assert( pLtlNode->left ); assert( pLtlNode->right == NULL ); 
-                leftAigObj = buildLogicFromLTLNode_combinationalOnly( pAigNew, pLtlNode->left );
-                assert( leftAigObj );
-                pLtlNode->pObj = Aig_Not( leftAigObj );
-                return pLtlNode->pObj;
-            case GLOBALLY:
-            case EVENTUALLY:
-            case NEXT:
-            case UNTIL:
-                printf("FORBIDDEN node: ABORTING!!\n");
-                exit(0);
-            default:
-                printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
-                exit(0);
-        }
-    }
-}
-
-Aig_Obj_t *buildLogicFromLTLNode( Aig_Man_t *pAig, ltlNode *pLtlNode )
-{
-    Aig_Obj_t *leftAigObj, *rightAigObj;
-
-    if( pLtlNode->pObj != NULL )
-        return pLtlNode->pObj;
-    else
-    {
-        assert( pLtlNode->type != BOOL );
-        switch( pLtlNode->type ){
-            case AND:
-                assert( pLtlNode->left ); assert( pLtlNode->right );
-                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
-                rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
-                assert( leftAigObj ); assert( rightAigObj );
-                pLtlNode->pObj = Aig_And( pAig, leftAigObj, rightAigObj );
-                return pLtlNode->pObj;
-            case OR:
-                assert( pLtlNode->left ); assert( pLtlNode->right );
-                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
-                rightAigObj = buildLogicFromLTLNode( pAig, pLtlNode->right );
-                assert( leftAigObj ); assert( rightAigObj );
-                pLtlNode->pObj = Aig_Or( pAig, leftAigObj, rightAigObj );
-                return pLtlNode->pObj;
-            case NOT:
-                assert( pLtlNode->left ); assert( pLtlNode->right == NULL ); 
-                leftAigObj = buildLogicFromLTLNode( pAig, pLtlNode->left );
-                assert( leftAigObj );
-                pLtlNode->pObj = Aig_Not( leftAigObj );
-                return pLtlNode->pObj;
-            case GLOBALLY:
-            case EVENTUALLY:
-            case NEXT:
-            case UNTIL:
-                printf("\nAttempting to create circuit with missing AIG pointer in a TEMPORAL node: ABORTING!!\n");
-                exit(0);
-            default:
-                printf("\nSerious ERROR: attempting to create AIG node from a temporal node\n");
-                exit(0);
-        }
-    }
-}
-
-int isNonTemporalSubformula( ltlNode *topNode )
-{
-    switch( topNode->type ){
-        case AND:
-        case OR:
-        case IMPLY:
-            return isNonTemporalSubformula( topNode->left) && isNonTemporalSubformula( topNode->right ) ;
-        case NOT:
-            assert( topNode->right == NULL );
-            return isNonTemporalSubformula( topNode->left );
-        case BOOL:
-            return 1;
-        default:
-            return 0;
-    }
-}
-
-int isWellFormed( ltlNode *topNode )
-{
-    ltlNode *nextNode;
-
-    switch( topNode->type ){
-        case AND:
-        case OR:
-        case IMPLY:
-            return isWellFormed( topNode->left) && isWellFormed( topNode->right ) ;
-        case NOT:
-            assert( topNode->right == NULL );
-            return isWellFormed( topNode->left );
-        case BOOL:
-            return 1;
-        case GLOBALLY:
-            nextNode = topNode->left;
-            assert( topNode->right == NULL );
-            if( nextNode->type != EVENTUALLY )
-                return 0;
-            else
-            {
-                assert( nextNode->right == NULL );
-                return isNonTemporalSubformula( nextNode->left );
-            }
-        default:
-            return 0;
-    }
-}
-
-int checkBooleanConstant( char *targetName )
-{
-    if( strcmp( targetName, "true" ) == 0 ) 
-        return 1;
-    if( strcmp( targetName, "false" ) == 0 )
-        return 0;
-    return -1;
-}
-
-int checkSignalNameExistence( Abc_Ntk_t *pNtk, ltlNode *topASTNode )
-{
-    char *targetName;
-    Abc_Obj_t * pNode;
-    int i;
-        
-    switch( topASTNode->type ){
-        case BOOL:
-            targetName = topASTNode->name;
-            //printf("\nTrying to match name %s\n", targetName);
-            if( checkBooleanConstant( targetName ) != -1 )
-                return 1;
-            Abc_NtkForEachPo( pNtk, pNode, i )
-            {
-                if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
-                {
-                    //printf("\nVariable name \"%s\" MATCHED\n", targetName);
-                    return 1;
-                }
-            }
-            printf("\nVariable name \"%s\" not found in the PO name list\n", targetName);
-            return 0;
-        case AND:
-        case OR:
-        case IMPLY:
-        case UNTIL:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right != NULL );
-            return checkSignalNameExistence( pNtk, topASTNode->left ) && checkSignalNameExistence( pNtk, topASTNode->right );
-            
-        case NOT:
-        case NEXT:
-        case GLOBALLY:
-        case EVENTUALLY:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right == NULL );
-            return checkSignalNameExistence( pNtk, topASTNode->left );
-        default:
-            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
-            exit(0);
-    }
-}
-
-void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, ltlNode *topASTNode )
-{
-    char *targetName;
-    Abc_Obj_t * pNode;
-    int i;
-    Aig_Obj_t *pObj, *pDriverImage;
-    
-    switch( topASTNode->type ){
-        case BOOL:
-            targetName = topASTNode->name;
-            if( checkBooleanConstant( targetName ) == 1 )
-            {
-                topASTNode->pObj = Aig_ManConst1( pAigNew );
-                return;
-            }
-            if( checkBooleanConstant( targetName ) == 0 )
-            {
-                topASTNode->pObj = Aig_Not(topASTNode->pObj = Aig_ManConst1( pAigNew ));
-                return;
-            }
-            Abc_NtkForEachPo( pNtk, pNode, i )
-                if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 )
-                {
-                    pObj = Aig_ManPo( pAigOld, i );
-                    assert( Aig_ObjIsPo( pObj ));
-                    pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj));
-                    topASTNode->pObj = pDriverImage;
-                    return;
-                }
-            assert(0);
-        case AND:
-        case OR:
-        case IMPLY:
-        case UNTIL:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right != NULL );
-            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
-            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->right );
-            return;
-        case NOT:
-        case NEXT:
-        case GLOBALLY:
-        case EVENTUALLY:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right == NULL );
-            populateBoolWithAigNodePtr( pNtk, pAigOld, pAigNew, topASTNode->left );
-            return;
-        default:
-            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
-            exit(0);
-    }
-}
-
-int checkAllBoolHaveAIGPointer( ltlNode *topASTNode )
-{
-    
-    switch( topASTNode->type ){
-        case BOOL:
-            if( topASTNode->pObj != NULL )
-                return 1;
-            else
-            {
-                printf("\nfaulting PODMANDYO topASTNode->name = %s\n", topASTNode->name);
-                return 0;
-            }
-        case AND:
-        case OR:
-        case IMPLY:
-        case UNTIL:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right != NULL );
-            return checkAllBoolHaveAIGPointer( topASTNode->left ) && checkAllBoolHaveAIGPointer( topASTNode->right );
-            
-        case NOT:
-        case NEXT:
-        case GLOBALLY:
-        case EVENTUALLY:
-            assert( topASTNode->left != NULL );
-            assert( topASTNode->right == NULL );
-            return checkAllBoolHaveAIGPointer( topASTNode->left );
-        default:
-            printf("\nUNSUPPORTED LTL NODE TYPE:: Aborting execution\n");
-            exit(0);
-    }
-}
-
-void setAIGNodePtrOfGloballyNode( ltlNode *astNode, Aig_Obj_t *pObjLo )
-{
-    astNode->pObj = pObjLo;
-}
-            
-Aig_Obj_t *retriveAIGPointerFromLTLNode( ltlNode *astNode )
-{
-    return astNode->pObj;
-}
-
-
-ABC_NAMESPACE_IMPL_END
diff --git a/src/aig/live/module.make b/src/aig/live/module.make
deleted file mode 100644
index 46a9ed3c..00000000
--- a/src/aig/live/module.make
+++ /dev/null
@@ -1,3 +0,0 @@
-SRC +=  src/aig/live/liveness.c \
-    src/aig/live/liveness_sim.c \
-    src/aig/live/ltl_parser.c