diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-07 18:11:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-07 18:11:29 -0700 |
| commit | a735d95a5bfa8ab21ddbe5a2a66695327d3b7206 (patch) | |
| tree | 96f083283877e8d8e8695aae7cf4101afc3cf6da /src/proof/ssc/sscCore.c | |
| parent | 51db560206d030e3f0b7628169a92ce58c601db7 (diff) | |
| download | abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.tar.gz abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.tar.bz2 abc-a735d95a5bfa8ab21ddbe5a2a66695327d3b7206.zip | |
SAT sweeping under constraints (bug fix).
Diffstat (limited to 'src/proof/ssc/sscCore.c')
| -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" ); |