summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmc3.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-03-17 22:48:05 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-03-17 22:48:05 -0700
commitaf0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf (patch)
tree72c8f3fccf909243001edd37ef511f0e9fb1f0af /src/sat/bmc/bmcBmc3.c
parent455ecb6accf2ce3c000cc04454e97f04ba20c6c1 (diff)
downloadabc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.tar.gz
abc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.tar.bz2
abc-af0ff7e6fa668b507bfb78baf1bcb1fa9d5e81bf.zip
Adding progress report to 'bmc3'.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
-rw-r--r--src/sat/bmc/bmcBmc3.c10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index bee14df2..8e983a2d 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -68,6 +68,14 @@ struct Gia_ManBmc_t_
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
+void Gia_ManReportProgress( FILE * pFile, int prop_no, int depth )
+{
+ extern int Gia_ManToBridgeProgress( FILE * pFile, int Size, unsigned char * pBuffer );
+ char buf[100];
+ sprintf(buf, "property: safe<%d>\nbug-free-depth: %d\n", prop_no, depth);
+ Gia_ManToBridgeProgress(pFile, strlen(buf), buf);
+}
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -1565,6 +1573,8 @@ nTimeUnsat += Abc_Clock() - clk2;
// propagate units
sat_solver_compress( p->pSat );
}
+ if ( p->pPars->fUseBridge )
+ Gia_ManReportProgress( stdout, i, f );
}
else if ( status == l_True )
{