summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satProof.c6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 93232f08..5616fdda 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -458,9 +458,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
}
Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) );
Vec_PtrFree( vUsed );
-
- Sat_ProofCheck0( vProof );
-
+
// report the result
if ( fVerbose )
{
@@ -474,6 +472,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
Vec_SetShrink( vProof, Vec_SetHandCurrentS(vProof) );
Vec_SetShrinkLimits( vProof );
// Sat_ProofReduceCheck( s );
+
+ Sat_ProofCheck0( vProof );
return RetValue;
}