summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmc3.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-10-26 23:05:13 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-10-26 23:05:13 -0700
commit3b30fb2a1189e7347c0cef2d0582a27bda4c125f (patch)
treed3ca7d8267e2d0e0b8c6e031f3ed27e4cd3b2eb4 /src/sat/bmc/bmcBmc3.c
parent9437664596a5fddc7faf2d3072c9c83d0eb2ff4d (diff)
downloadabc-3b30fb2a1189e7347c0cef2d0582a27bda4c125f.tar.gz
abc-3b30fb2a1189e7347c0cef2d0582a27bda4c125f.tar.bz2
abc-3b30fb2a1189e7347c0cef2d0582a27bda4c125f.zip
Multi-output property solver.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
-rw-r--r--src/sat/bmc/bmcBmc3.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ea08c1e4..4cc2a692 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1353,7 +1353,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
goto finish;
}
// consider the next timeframe
- if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
+ if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
pPars->iFrame = f-1;
// map nodes of this section
Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );