diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-27 00:48:06 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-27 00:48:06 -0800 |
| commit | ce0e8caf79b596423272aa5d9d4aeb931aa88259 (patch) | |
| tree | e6334ce2cfbf44909f218f4efb7ffbf0c65f347f /src/aig/saig | |
| parent | c7e855619a1ea5997b68a235c27187a1b43252dc (diff) | |
| download | abc-ce0e8caf79b596423272aa5d9d4aeb931aa88259.tar.gz abc-ce0e8caf79b596423272aa5d9d4aeb931aa88259.tar.bz2 abc-ce0e8caf79b596423272aa5d9d4aeb931aa88259.zip | |
Variable timeframe abstraction.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigGlaPba2.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 8bc2b982..55aa0a3d 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -308,7 +308,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p ) Vec_IntPush( p->vCla2Fra, 0 ); assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) ); assert( nVars == Vec_IntSize(p->vVar2Inf) ); - assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses ); + assert( Vec_IntSize(p->vCla2Obj) == (int)p->pSat->stats.clauses+1 ); if ( p->fVerbose ) printf( "The resulting SAT problem contains %d variables and %d clauses.\n", p->pSat->size, p->pSat->stats.clauses ); @@ -337,8 +337,8 @@ Aig_Gla3Man_t * Aig_Gla3ManStart( Aig_Man_t * pAig, int nStart, int nFramesMax, p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); p->vVec2Var = Vec_IntAlloc( 1 << 20 ); p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); - p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); - p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); + p->vCla2Obj = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Obj, -1 ); + p->vCla2Fra = Vec_IntAlloc( 1 << 20 ); Vec_IntPush( p->vCla2Fra, -1 ); // skip first vector ID p->nStart = nStart; |