summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/pdr/pdrInv.c2
-rw-r--r--src/sat/pdr/pdrMan.c4
2 files changed, 3 insertions, 3 deletions
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
index 184b6c4f..5eb32790 100644
--- a/src/sat/pdr/pdrInv.c
+++ b/src/sat/pdr/pdrInv.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
+#include "extra.h"
ABC_NAMESPACE_IMPL_START
@@ -44,7 +45,6 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
{
- extern int Extra_Base10Log( unsigned int Num );
static int PastSize;
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
index f33f6586..789f4ce8 100644
--- a/src/sat/pdr/pdrMan.c
+++ b/src/sat/pdr/pdrMan.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
+#include "ssw.h"
ABC_NAMESPACE_IMPL_START
@@ -157,7 +158,6 @@ void Pdr_ManStop( Pdr_Man_t * p )
***********************************************************************/
Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
{
- extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
Abc_Cex_t * pCex;
Pdr_Obl_t * pObl;
int i, f, Lit, nFrames = 0;
@@ -165,7 +165,7 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
nFrames++;
// create the counter-example
- pCex = Gia_ManAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
+ pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )