1 files changed, 48 insertions, 4 deletions

diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 35029034..cf04ab62 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -75,6 +75,34 @@ Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut,
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of constant 0 POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCountConst0PosGia( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachPo( p, pObj, i )
+        Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
+    return Counter;
+}
+int Gia_ManCountConst0Pos( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Saig_ManForEachPo( p, pObj, i )
+        Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -138,18 +166,23 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
     Vec_Ptr_t * vCexes;
     Aig_Man_t * pTemp;
     abctime clkStart = Abc_Clock();
-    int nTimeToStop  = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
     int nTotalPo     = Saig_ManPoNum(p);
     int nTotalSize   = Aig_ManObjNum(p);
     int TimeOutLoc   = pPars->TimeOutLoc;
     int i, RetValue  = -1;
     if ( pPars->fVerbose )
-        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", 
+            pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+    if ( pPars->fVerbose )
+        printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", 
+            pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
     // create output map
     vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
     vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
     for ( i = 0; i < 1000; i++ )
     {
+        int nSolved = Vec_PtrCountZero(vCexes);
         // perform SIM3
         Ssw_RarSetDefaultParams( pParsSim );
         pParsSim->fSolveAll = 1;
@@ -157,6 +190,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
         pParsSim->fSilent = !pPars->fVeryVerbose;
         pParsSim->TimeOut = TimeOutLoc;
         pParsSim->nRandSeed = (i * 17) % 500;
+        pParsSim->nWords = 5;
         RetValue *= Ssw_RarSimulate( p, pParsSim );
         // sort outputs
         if ( p->vSeqModelVec )
@@ -173,7 +207,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
             Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
 
         // check timeout
-        if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
         {
             printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
             break;
@@ -185,6 +219,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
         pParsBmc->fNotVerbose = 1;
         pParsBmc->fSilent = !pPars->fVeryVerbose;
         pParsBmc->nTimeOut = TimeOutLoc;
+        pParsBmc->nTimeOutOne = pPars->TimePerOut;
         RetValue *= Saig_ManBmcScalable( p, pParsBmc );
         if ( pPars->fVeryVerbose )
             Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", 
@@ -204,12 +239,19 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
             Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
 
         // check timeout
-        if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
         {
             printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
             break;
         }
 
+        // check gap timeout
+        if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
+        {
+            printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
+            break;
+        }
+
         // synthesize
         if ( pPars->fUseSyn )
         {
@@ -223,6 +265,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
         TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
     }
     Vec_IntFree( vOutMap );
+    if ( pPars->fVerbose )
+        printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
     if ( pPars->fDumpFinal )
     {
         char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );