From e91abd6307e15d9d4a4985146025e12ae6780cff Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Feb 2017 16:03:40 -0800 Subject: Improvements to inductive generalization in IC3/PDR by Zyad Hassan. --- src/proof/pdr/pdrTsim.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/proof/pdr/pdrTsim.c') 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; } -- cgit v1.2.3