From 3b30fb2a1189e7347c0cef2d0582a27bda4c125f Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 26 Oct 2013 23:05:13 -0700
Subject: Multi-output property solver.

---
 src/sat/bmc/bmcBmc3.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/sat/bmc/bmcBmc3.c')

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) );
-- 
cgit v1.2.3