summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
-rw-r--r--src/proof/pdr/pdrCore.c5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 20db8f67..78cc16c1 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
+#include "base/main/main.h"
ABC_NAMESPACE_IMPL_START
@@ -910,6 +911,10 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
RetValue = Pdr_ManSolveInt( p );
if ( RetValue == 0 )
assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
+ if ( RetValue == 1 )
+ Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
+ else
+ Abc_FrameSetInv( NULL );
if ( p->vCexes )
{
assert( p->pAig->vSeqModelVec == NULL );