From 32288c696493a223966ed334554f0a113d9134f0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Jan 2017 14:02:14 -0800 Subject: Adding features for invariant minimization. --- src/proof/pdr/pdrCore.c | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index c625e366..b81a1a2a 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -926,6 +926,8 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); Pdr_ManDumpClauses( p, pFileName, RetValue==1 ); } + else if ( RetValue == 1 ) + Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); p->tTotal += Abc_Clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; -- cgit v1.2.3