diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
commit | 65687f72ae77440628c21d63966656c1049c4981 (patch) | |
tree | 27a4c7800e372349f1521daac76c0b30e2578ca1 /src/aig/fra/fraInd.c | |
parent | 369f008e69a4f201cbc7c890a08221086bee4698 (diff) | |
download | abc-65687f72ae77440628c21d63966656c1049c4981.tar.gz abc-65687f72ae77440628c21d63966656c1049c4981.tar.bz2 abc-65687f72ae77440628c21d63966656c1049c4981.zip |
Version abc71208
Diffstat (limited to 'src/aig/fra/fraInd.c')
-rw-r--r-- | src/aig/fra/fraInd.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 6cfdc3ff..dbc6401f 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -339,7 +339,7 @@ PRT( "Time", clock() - clk ); // Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" ); // Fra_ManPartitionTest2( pManAigNew ); // Aig_ManStop( pManAigNew ); - + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -365,7 +365,7 @@ p->timeTrav += clock() - clk2; pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); - p->pSat = Cnf_DataWriteIntoSolver( pCnf ); + p->pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->nSatVars = pCnf->nVars; assert( p->pSat != NULL ); if ( p->pSat == NULL ) |