Version abc80702

4 files changed, 12 insertions, 16 deletions

diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index 889e6298..afc4a34a 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -151,7 +151,8 @@ Aig_Man_t * Saig_ManDuplicated( Aig_Man_t * p )
 Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pCtrl;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
     int i;
     assert( Aig_ManRegNum(p) > 0 );
     // create the new manager
@@ -583,12 +584,6 @@ p->timeCnf += clock() - clk;
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
                     i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
                 PRT( "Time", clock() - clk );
-                if ( Aig_ManNodeNum(p->pInter) == 0 )
-                {
-                    Aig_Obj_t * pObj = Aig_ManPo(p->pInter, 0);
-                    Aig_Obj_t * pObjR = Aig_Regular(pObj);
-                    int x = 0;
-                }
             }
             if ( RetValue == 0 ) // found a (spurious?) counter-example
             {
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 0ad6c314..1820ae9a 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -150,13 +150,14 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
         printf( "\n" );
     }
     // collect the nodes
-    if ( fVeryVerbose )
-    Aig_ManForEachObj( p, pObj, i )
-        if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
-        {
-            Aig_ObjPrint( p, pObj );
-            printf( "\n" );
-        }
+    if ( fVeryVerbose ) {
+      Aig_ManForEachObj( p, pObj, i )
+          if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
+          {
+              Aig_ObjPrint( p, pObj );
+              printf( "\n" );
+          }
+    }
     // pick the first PO in the list
     nPos = 0;
     iBadPo = -1;
diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c
index 67e3e95b..6d55943a 100644
--- a/src/aig/saig/saigScl.c
+++ b/src/aig/saig/saigScl.c
@@ -82,7 +82,7 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
 int Saig_ManReportComplements( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj, * pFanin;
-    int i, Counter = 0, Diffs = 0;
+    int i, Counter = 0;
     assert( Aig_ManRegNum(p) > 0 );
     Aig_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA );
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index b0039276..c1c2d8e9 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -375,7 +375,7 @@ Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFrame
 {
     extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
     Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
-    int clk, clkTotal = clock();
+    int clk;
     // create uninitialized timeframes with map1
     pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
     // perform fraiging for the unrolled timeframes