diff options
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 64ea44b0..017c9407 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1760,7 +1760,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) Gla_Man_t * p; Vec_Int_t * vCore, * vPPis; Abc_Cex_t * pCex = NULL; - int f, i, iPrev, nConfls, Status, nCoreSize, fOneIsSent = 0, RetValue = -1; + int f, i, iPrev, nConfls, Status, nVarsOld, nCoreSize, fOneIsSent = 0, RetValue = -1; clock_t clk = clock(), clk2; // preconditions assert( Gia_ManPoNum(pAig) == 1 ); @@ -1827,6 +1827,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) sat_solver2_bookmark( p->pSat ); Vec_IntClear( p->vAddedNew ); p->nAbsOld = Vec_IntSize( p->vAbs ); + nVarsOld = p->nSatVars; // iterate as long as there are counter-examples for ( i = 0; ; i++ ) @@ -1904,6 +1905,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // update storage Gla_ManRollBack( p ); Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 ); + p->nSatVars = nVarsOld; // load this timeframe Gia_GlaAddToAbs( p, vCore, 0 ); Gia_GlaAddOneSlice( p, f, vCore ); |