summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/pdr/pdrInv.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 0d27ce7e..8b04c53b 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -759,14 +759,14 @@ int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver
if ( status == l_False ) // unsat -- correct
continue;
assert( status == l_True );
+ if ( fVerbose )
+ printf( "Inductiveness check failed for clause %d.\n", i );
nFailed++;
if ( fSkip )
{
Vec_IntFree( vLits );
return 1;
}
- if ( fVerbose )
- printf( "Inductiveness check failed for clause %d.\n", i );
}
Vec_IntFree( vLits );
return nFailed + nFailedOuts;