diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-01 10:50:50 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-01 10:50:50 +0700 |
| commit | 7884dd01bc07b4f052436f996eee3cb66169a556 (patch) | |
| tree | 550a4c2597981b91682f9c16595bd7b2aabd6a59 /src/aig/fra | |
| parent | dbe2b466d79fb550275c4334697ea600acd66036 (diff) | |
| download | abc-7884dd01bc07b4f052436f996eee3cb66169a556.tar.gz abc-7884dd01bc07b4f052436f996eee3cb66169a556.tar.bz2 abc-7884dd01bc07b4f052436f996eee3cb66169a556.zip | |
Fixed a corner case bug in dprove when a trivial CEX is not produced.
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fraSec.c | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index ca8cf799..3b28936d 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -620,6 +620,17 @@ ABC_PRT( "Time", clock() - clkTotal ); } else if ( RetValue == 0 ) { + if ( pNew->pSeqModel == NULL ) + { + int i; + // if the CEX is not derives, it is because tricial CEX should be assumed + pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 ); + // if the CEX does not work, we need to change PIs to 1 because + // the only way it can happen is when a PO is equal to a PI... + if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 ) + for ( i = 0; i < pNew->nTruePis; i++ ) + Aig_InfoSetBit( pNew->pSeqModel->pData, i ); + } if ( !pParSec->fSilent ) { printf( "Networks are NOT EQUIVALENT. " ); |