summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/pdr/pdrCore.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index c625e366..b81a1a2a 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -926,6 +926,8 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
+ else if ( RetValue == 1 )
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
p->tTotal += Abc_Clock() - clk;
Pdr_ManStop( p );
pPars->iFrame--;