summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrMan.c
diff options
context:
space:
mode:
authorBruno Schmitt <bruno@oschmitt.com>2017-02-15 17:19:52 -0800
committerBruno Schmitt <bruno@oschmitt.com>2017-02-15 17:19:52 -0800
commit7811f1bb07eea98eaafcdeb56d159bf5e369b4b0 (patch)
tree27821c0804ae90a0b49ee1fc7172c4724a7f8d43 /src/proof/pdr/pdrMan.c
parent088aabc1023e6745bedeb16f9f8f01515c38e4b7 (diff)
parentab387953ab3a50200384f5619cf999e3f729f28f (diff)
downloadabc-7811f1bb07eea98eaafcdeb56d159bf5e369b4b0.tar.gz
abc-7811f1bb07eea98eaafcdeb56d159bf5e369b4b0.tar.bz2
abc-7811f1bb07eea98eaafcdeb56d159bf5e369b4b0.zip
Merged alanmi/abc into default
Diffstat (limited to 'src/proof/pdr/pdrMan.c')
-rw-r--r--src/proof/pdr/pdrMan.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index c19041ee..abe8c0a8 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -455,7 +455,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
int i, f, Lit, Flop, nFrames = 0;
int nPis = Saig_ManPiNum(p->pAig);
int nFfRefined = 0;
- if ( !p->pPars->fUseAbs )
+ if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
return Pdr_ManDeriveCex(p);
// restore previous map
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )