diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-26 21:29:57 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-10-26 21:29:57 -0700 |
| commit | 9437664596a5fddc7faf2d3072c9c83d0eb2ff4d (patch) | |
| tree | d638e36e7c05115d1bf049ba1a305804d34e099c /src/proof | |
| parent | 7d2b77afc86031ec31bd952391db9c2e45b64cd7 (diff) | |
| download | abc-9437664596a5fddc7faf2d3072c9c83d0eb2ff4d.tar.gz abc-9437664596a5fddc7faf2d3072c9c83d0eb2ff4d.tar.bz2 abc-9437664596a5fddc7faf2d3072c9c83d0eb2ff4d.zip | |
Multi-output property solver.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index cd93d28b..39f95e14 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -1054,7 +1054,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) if ( !pPars->fSilent ) { if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" ); - Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved ); Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut ); } goto finish; @@ -1064,7 +1064,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) if ( !pPars->fSilent ) { if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" ); - Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved ); Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap ); } goto finish; |