diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-28 10:49:59 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-28 10:49:59 -0700 |
| commit | 0f1624e5d218cda55a8526c9338f68b2122b86fd (patch) | |
| tree | 5ad99908dffff9047db289c4e7a909fd9c6f9f45 /src/proof | |
| parent | 1bb918167e2c2822eef8b1ea708bfb51ef70e6d1 (diff) | |
| download | abc-0f1624e5d218cda55a8526c9338f68b2122b86fd.tar.gz abc-0f1624e5d218cda55a8526c9338f68b2122b86fd.tar.bz2 abc-0f1624e5d218cda55a8526c9338f68b2122b86fd.zip | |
The same bug fix in 'scorr -c' (signal correspondence with constraints).
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/ssw/sswConstr.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index a9ed17fc..a3a7e66f 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -533,8 +533,10 @@ clk = Abc_Clock(); continue; } Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) ); - } - + } + // sweep flops + Saig_ManForEachLo( p->pAig, pObj, i ) + p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { |