diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-25 14:02:14 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-25 14:02:14 -0800 |
| commit | 32288c696493a223966ed334554f0a113d9134f0 (patch) | |
| tree | 363e7284a931509e27c4fe8ab33b6021ebf9f038 | |
| parent | 3119e1e30f8a44eb6236792c69f8cca64c99f7a8 (diff) | |
| download | abc-32288c696493a223966ed334554f0a113d9134f0.tar.gz abc-32288c696493a223966ed334554f0a113d9134f0.tar.bz2 abc-32288c696493a223966ed334554f0a113d9134f0.zip | |
Adding features for invariant minimization.
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 2 |
1 files changed, 2 insertions, 0 deletions
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--; |