From 291f1ee054b6a1746d7af208a0d6ff361a0fe71a Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 9 Jul 2012 22:16:23 -0700
Subject: Performance bug fix in &gla.

---
 src/aig/gia/giaAbsGla.c | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

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