diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-16 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-16 08:01:00 -0800 |
commit | 126637ddd3c237d9c83f3a7f2b1f3f2722337411 (patch) | |
tree | bcc45e2a3b8cde987c42e85edeca3e64ba417456 /src/aig/fra/fraClau.c | |
parent | 65687f72ae77440628c21d63966656c1049c4981 (diff) | |
download | abc-126637ddd3c237d9c83f3a7f2b1f3f2722337411.tar.gz abc-126637ddd3c237d9c83f3a7f2b1f3f2722337411.tar.bz2 abc-126637ddd3c237d9c83f3a7f2b1f3f2722337411.zip |
Version abc71216
Diffstat (limited to 'src/aig/fra/fraClau.c')
-rw-r--r-- | src/aig/fra/fraClau.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c index ea8406c7..fc239a40 100644 --- a/src/aig/fra/fraClau.c +++ b/src/aig/fra/fraClau.c @@ -227,7 +227,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) p->vCexBmc = Vec_IntAlloc( Aig_ManRegNum(pMan) ); // derive two timeframes to be checked - pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs + pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs //Aig_ManShow( pFramesMain, 0, NULL ); assert( Aig_ManPoNum(pFramesMain) == 2 ); Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output @@ -245,14 +245,14 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) */ // derive one timeframe to be checked - pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL ); + pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL ); assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); // derive one timeframe to be checked for BMC - pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL ); + pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL ); //Aig_ManShow( pFramesBmc, 0, NULL ); assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); |