diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-04-22 19:14:22 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-04-22 19:14:22 -0700 |
| commit | 74d0ffee6977c24ee8f3c4fa1471f98f6455d5bb (patch) | |
| tree | 56cadb3a4e68e4dbcf02858880a53984a0e9c10d /src/proof/cec | |
| parent | c4911370bbcf09e675e61ff49117bc91cc92ebc1 (diff) | |
| download | abc-74d0ffee6977c24ee8f3c4fa1471f98f6455d5bb.tar.gz abc-74d0ffee6977c24ee8f3c4fa1471f98f6455d5bb.tar.bz2 abc-74d0ffee6977c24ee8f3c4fa1471f98f6455d5bb.zip | |
Misc changes.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecCec.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index aa36a28e..b9b3e1f1 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -143,7 +143,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) // (for example, when they have the same driver but complemented) if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different phase). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); @@ -155,7 +155,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) // drivers are different PIs if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different PIs). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); @@ -168,7 +168,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) || (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) ) { - Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 ); + Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (PI vs. constant). ", i/2 ); Abc_PrintTime( 1, "Time", clock() - clk ); pPars->iOutFail = i/2; Cec_ManTransformPattern( p, i/2, NULL ); |