diff options
Diffstat (limited to 'src/proof/ssc')
| -rw-r--r-- | src/proof/ssc/sscCore.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index 43d0e250..1a57a47c 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -298,6 +298,7 @@ clk = clock(); { p->nSatCallsUnsat++; pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ); + Gia_ObjSetProved( pAig, i ); } else if ( status == l_True ) { @@ -329,9 +330,10 @@ clk = clock(); p->timeSimSat += clock() - clk; } // Gia_ManEquivPrintClasses( pAig, 1, 0 ); +// Gia_ManPrint( pAig ); // generate the resulting AIG - pResult = Gia_ManEquivReduce( pAig, 1, 0, 0 ); + pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 ); if ( pResult == NULL ) { printf( "There is no equivalences.\n" ); |