summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/ssc/sscCore.c4
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" );