From cb99a2212df80a324ffae67c804f50079336dcd4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 5 Aug 2013 22:58:08 -0700 Subject: Bug fix in 'int'. --- src/sat/bsat/satInterA.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index f13d2666..c769352f 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -603,7 +603,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF // resolve the temporary resolvent with the reason clause if ( p->fProofVerif ) { - int v1, v2, Entry; + int v1, v2, Entry = -1; if ( fPrint ) Inta_ManPrintResolvent( p->vResLits ); // check that the var is present in the resolvent @@ -649,7 +649,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF // use the resulting clause to check the correctness of resolution if ( p->fProofVerif ) { - int v1, v2, Entry; + int v1, v2, Entry = -1; if ( fPrint ) Inta_ManPrintResolvent( p->vResLits ); Vec_IntForEachEntry( p->vResLits, Entry, v1 ) -- cgit v1.2.3