From 57286e8ab692d2df5df6e4077134b913229ba33f Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 25 Jan 2017 22:29:51 -0800
Subject: Adding features for invariant minimization.

---
 src/proof/pdr/pdrInv.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/proof/pdr/pdrInv.c')

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;
-- 
cgit v1.2.3