diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-08-05 22:58:08 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-08-05 22:58:08 -0700 |
| commit | cb99a2212df80a324ffae67c804f50079336dcd4 (patch) | |
| tree | 3407f165cecd82c4db404b52e52d2ce6d9102390 /src/sat/bsat | |
| parent | 220a83f1e5007f38df9c798298652bcb837fc002 (diff) | |
| download | abc-cb99a2212df80a324ffae67c804f50079336dcd4.tar.gz abc-cb99a2212df80a324ffae67c804f50079336dcd4.tar.bz2 abc-cb99a2212df80a324ffae67c804f50079336dcd4.zip | |
Bug fix in 'int'.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satInterA.c | 4 |
1 files 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 ) |