diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-02 16:03:40 -0800 |
| commit | e91abd6307e15d9d4a4985146025e12ae6780cff (patch) | |
| tree | c4425a5f5686587b6fcf29a582412363537e23a1 /src/proof/pdr/pdrTsim.c | |
| parent | f14ee271abe8d38a6dad8789d4b4dbc207fe23c4 (diff) | |
| download | abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.gz abc-e91abd6307e15d9d4a4985146025e12ae6780cff.tar.bz2 abc-e91abd6307e15d9d4a4985146025e12ae6780cff.zip | |
Improvements to inductive generalization in IC3/PDR by Zyad Hassan.
Diffstat (limited to 'src/proof/pdr/pdrTsim.c')
| -rw-r--r-- | src/proof/pdr/pdrTsim.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 32d1c857..37f84667 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -476,7 +476,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); assert( Vec_IntSize(vRes) > 0 ); p->tTsim += Abc_Clock() - clk; pRes = Pdr_SetCreate( vRes, vPiLits ); - assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); + //ZH: Disabled assertion because this invariant doesn't hold with down + //because of the join operation which can bring in initial states + //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); return pRes; } |