summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrCore.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-01-06 11:52:00 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-01-06 11:52:00 +0700
commita2fcd0710d22d79ef238e1cb9ef328ce94fa5000 (patch)
tree65ed96ef1be0f68e6d172e85358f897e5eda24d5 /src/proof/pdr/pdrCore.c
parente9a7ad68c4c2f2b95695875996e713f7ae708912 (diff)
downloadabc-a2fcd0710d22d79ef238e1cb9ef328ce94fa5000.tar.gz
abc-a2fcd0710d22d79ef238e1cb9ef328ce94fa5000.tar.bz2
abc-a2fcd0710d22d79ef238e1cb9ef328ce94fa5000.zip
Creating file name from design name for PDR invariant.
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
-rw-r--r--src/proof/pdr/pdrCore.c3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index c020c56a..66cae36e 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -922,10 +922,11 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
}
if ( p->pPars->fDumpInv )
{
+ char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Abc_FrameSetStr( Pdr_ManDumpString(p) );
Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
- Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
+ Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
p->tTotal += Abc_Clock() - clk;
Pdr_ManStop( p );