From 0d65c49048eea6940e3f5fa9bbf28ee5c6b97102 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 31 Jul 2011 20:22:57 +0700
Subject: Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop
 when 2^nRegs frames are completed).

---
 src/base/abci/abcDar.c | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'src/base/abci/abcDar.c')

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c0822ba9..064529cc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1805,8 +1805,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( RetValue == 1 )
     {
-//        printf( "No output asserted in %d frames. ", pPars->iFrame );
-        printf( "Incorrect return value.  " );
+        printf( "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
     }
     else if ( RetValue == -1 )
     {
@@ -1839,8 +1838,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
         }
         else
         {
-            printf( "Incorrect return value.  " );
-//            printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
+            printf( "All %d outputs are proved SAT.    ", Saig_ManPoNum(pMan) - pMan->nConstrs );
         }
     }
     ABC_PRT( "Time", clock() - clk );
@@ -3044,8 +3042,8 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
     }
     else
     {
-        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
-            nFrames, nWords );
+//        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
+//            nFrames, nWords );
     }
     ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
-- 
cgit v1.2.3