Skip to content

A
abc
Commit cb99a221 by Alan Mishchenko
Options

Bug fix in 'int'.

parent 220a83f1
Showing with 2 additions and 2 deletions
src/sat/bsat/satInterA.c
...@@ -603,7 +603,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF ...@@ -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 // resolve the temporary resolvent with the reason clause
if ( p->fProofVerif ) if ( p->fProofVerif )
{ {
int v1, v2, Entry; int v1, v2, Entry = -1;
if ( fPrint ) if ( fPrint )
Inta_ManPrintResolvent( p->vResLits ); Inta_ManPrintResolvent( p->vResLits );
// check that the var is present in the resolvent // 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 ...@@ -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 // use the resulting clause to check the correctness of resolution
if ( p->fProofVerif ) if ( p->fProofVerif )
{ {
int v1, v2, Entry; int v1, v2, Entry = -1;
if ( fPrint ) if ( fPrint )
Inta_ManPrintResolvent( p->vResLits ); Inta_ManPrintResolvent( p->vResLits );
Vec_IntForEachEntry( p->vResLits, Entry, v1 ) Vec_IntForEachEntry( p->vResLits, Entry, v1 )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment