summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-08-16 14:20:52 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-08-16 14:20:52 +0700
commit23d36a8d5665d7a586777c9723c4aa803b253fc1 (patch)
tree69210b61d5602dac1dccdea7a62756e813adb1c4 /src/proof/ssw
parentd2747fb2815a4fea35a0bf23cb4941d61a1d99fc (diff)
downloadabc-23d36a8d5665d7a586777c9723c4aa803b253fc1.tar.gz
abc-23d36a8d5665d7a586777c9723c4aa803b253fc1.tar.bz2
abc-23d36a8d5665d7a586777c9723c4aa803b253fc1.zip
Integrating Satoko into 'bmc' and 'bmc2'.
Diffstat (limited to 'src/proof/ssw')
-rw-r--r--src/proof/ssw/sswRarity.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index a02ea01b..1b7cab23 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -1011,7 +1011,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
if ( fTryBmc )
{
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
- Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
+ Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0, 0 );
// if ( pNewAig->pSeqModel != NULL )
// Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
Aig_ManStop( pNewAig );