Changes to clause mapping.

src/aig/gia/giaAbsGla.c

@@ -1096,7 +1096,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
     // other 
-    p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
+    p->vCla2Obj  = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
 //    p->pSat->fVerbose = p->pPars->fVerbose;
 //    sat_solver2_set_learntmax( p->pSat, pPars->nLearnedMax );
@@ -1195,7 +1195,7 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
     // other 
-    p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
+    p->vCla2Obj  = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
     p->nSatVars  = 1;
     return p;
@@ -1914,7 +1914,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
             sat_solver2_rollback( p->pSat );
             // update storage
             Gla_ManRollBack( p );
-            Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
+            Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses );
             p->nSatVars = nVarsOld;
             // load this timeframe
             Gia_GlaAddToAbs( p, vCore, 0 );

src/aig/gia/giaAbsVta.c

@@ -1034,7 +1034,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->nSeenGla    = 1;
     p->nSeenAll    = 1;
     // other data
-    p->vCla2Var    = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Var, -1 );
+    p->vCla2Var    = Vec_IntAlloc( 1000 ); // Vec_IntPush( p->vCla2Var, -1 );
     p->vCores      = Vec_PtrAlloc( 100 );
     p->pSat        = sat_solver2_new();
 //    p->pSat->fVerbose = p->pPars->fVerbose;
@@ -1658,7 +1658,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         sat_solver2_rollback( p->pSat );
         // update storage
         Vga_ManRollBack( p, nObjOld );
-        Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
+        Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses );
         // load this timeframe
         Vga_ManLoadSlice( p, vCore, 0 );
         Vec_IntFree( vCore );

src/sat/bsat/satSolver2.h

@@ -160,7 +160,7 @@ struct sat_solver2_t
 };
 
 static inline clause * clause2_read( sat_solver2 * s, cla h )                  { return Sat_MemClauseHand( &s->Mem, h );   }
-static inline int      clause2_proofid(sat_solver2* s, clause* c, int partA)   { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : ((clause_id(c)+1)<<2) | (partA<<1) | 1; }
+static inline int      clause2_proofid(sat_solver2* s, clause* c, int partA)   { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (partA<<1) : (clause_id(c)<<2) | (partA<<1) | 1; }
 
 // these two only work after creating a clause before the solver is called
 static inline int   clause2_is_partA (sat_solver2* s, int h)                   { return clause2_read(s, h)->partA;         }