summaryrefslogtreecommitdiffstats
path: root/src/proof/bbr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/bbr')
-rw-r--r--src/proof/bbr/bbrNtbdd.c4
-rw-r--r--src/proof/bbr/bbrReach.c2
2 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/bbr/bbrNtbdd.c b/src/proof/bbr/bbrNtbdd.c
index 49c2873b..f61c3d73 100644
--- a/src/proof/bbr/bbrNtbdd.c
+++ b/src/proof/bbr/bbrNtbdd.c
@@ -135,7 +135,7 @@ int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p )
Aig_Obj_t * pObj;
int RetValue, i;
// complement the global functions
- vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
+ vFuncsGlob = Vec_PtrAlloc( Aig_ManCoNum(p) );
Aig_ManForEachCo( p, pObj, i )
Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
@@ -162,7 +162,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI
DdNode * bFunc;
int i, Counter;
// start the manager
- dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// set reordering
if ( fReorder )
Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c
index 1b5c3984..eda4d7cf 100644
--- a/src/proof/bbr/bbrReach.c
+++ b/src/proof/bbr/bbrReach.c
@@ -548,7 +548,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
return Aig_ManVerifyUsingBdds_int( pInit, pPars );
// create new AIG
p = Aig_ManDupTrim( pInit );
- assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
+ assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
if ( RetValue != 0 )