summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-11-09 23:13:37 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2014-11-09 23:13:37 -0800
commitac72d73dc6325410d2b69ee63eb727bfc42e46d9 (patch)
treead5256da9ffcdf40ec82e95d43994685349a0272 /src/proof
parent9a292bd93c84e7f9445d796fdd5f1ca86c9ea220 (diff)
downloadabc-ac72d73dc6325410d2b69ee63eb727bfc42e46d9.tar.gz
abc-ac72d73dc6325410d2b69ee63eb727bfc42e46d9.tar.bz2
abc-ac72d73dc6325410d2b69ee63eb727bfc42e46d9.zip
Removing unauthorized printout in 'pdr'.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/pdr/pdrCore.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 9789e7e0..20db8f67 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -619,6 +619,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
+ if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );