Integrating synthesis into the new BMC engine.

src/map/if/ifDec07.c

@@ -713,7 +713,7 @@ word If_Dec5Perform( word t, int fDerive )
 {
     int Pla2Var[7], Var2Pla[7];
     int i, j, v;
-    word t0 = t;
+//    word t0 = t;
     word c0, c1, c00, c01, c10, c11;
     for ( i = 0; i < 5; i++ )
     {

src/map/mio/mioParse.c

@@ -429,7 +429,7 @@ void Mio_ParseFormulaTruthTest( char * pFormInit, char ** ppVarNames, int nVars
 int Mio_ParseCheckName( Mio_Gate_t * pGate, char ** ppStr )
 {
     Mio_Pin_t * pPin;
-    int i, iBest;
+    int i, iBest = -1;
     // find the longest pin name that matches substring
     char * pNameBest = NULL;
     for ( pPin = Mio_GateReadPins(pGate), i = 0; pPin; pPin = Mio_PinReadNext(pPin), i++ )
@@ -437,9 +437,8 @@ int Mio_ParseCheckName( Mio_Gate_t * pGate, char ** ppStr )
             if ( pNameBest == NULL || strlen(pNameBest) < strlen(Mio_PinReadName(pPin)) )
                 pNameBest = Mio_PinReadName(pPin), iBest = i;
     // if pin is not found, return -1
-    if ( pNameBest == NULL )
-        return -1;
-    *ppStr += strlen(pNameBest) - 1;
+    if ( pNameBest )
+        *ppStr += strlen(pNameBest) - 1;
     return iBest;
 }
 int Mio_ParseCheckFormula( Mio_Gate_t * pGate, char * pForm )

src/sat/bmc/bmcBmcAnd.c

@@ -775,12 +775,6 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     abctime clk = Abc_Clock();
     p = Bmc_MnaAlloc();
     p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
-    if ( pPars->fUseSynth )
-    {
-        Gia_Man_t * pTemp = p->pFrames;
-        p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
-        Gia_ManStop( pTemp );
-    }
     nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
     if ( pPars->fVerbose )
     {
@@ -789,6 +783,14 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     }
     if ( pPars->fVerbose )
         Gia_ManPrintStats( p->pFrames, NULL );
+    if ( pPars->fUseSynth )
+    {
+        Gia_Man_t * pTemp = p->pFrames;
+        p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
+        Gia_ManStop( pTemp );
+        if ( pPars->fVerbose )
+            Gia_ManPrintStats( p->pFrames, NULL );
+    }
     if ( pPars->fDumpFrames )
     {
         Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );