summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-12-22 06:39:13 -1000
committerAlan Mishchenko <alanmi@berkeley.edu>2015-12-22 06:39:13 -1000
commit617055f5a2c8f85b145cf273888583e62a160315 (patch)
treedfa7a63780ceb2b158908640b5f761c9f583021e /src/proof/pdr
parent2e8543fca129fd149b419ccd2549046d95ba225f (diff)
downloadabc-617055f5a2c8f85b145cf273888583e62a160315.tar.gz
abc-617055f5a2c8f85b145cf273888583e62a160315.tar.bz2
abc-617055f5a2c8f85b145cf273888583e62a160315.zip
Adding names to GIA inputs/outputs. Changing polarity of invariant generated by PDR.
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/pdrInv.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 8750339e..860462c3 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -378,7 +378,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{
Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
- fprintf( pFile, " 0\n" );
+ fprintf( pFile, " 1\n" );
}
fprintf( pFile, ".e\n\n" );
fclose( pFile );