Version abc61206

3 files changed, 3 insertions, 59 deletions

diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 8f08eaff..585a5561 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -511,7 +511,6 @@ static inline void Extra_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned *
 extern void     Extra_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
 extern void     Extra_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
 extern void     Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase );
-extern DdNode * Extra_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
 extern int      Extra_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
 extern int      Extra_TruthSupportSize( unsigned * pTruth, int nVars );
 extern int      Extra_TruthSupport( unsigned * pTruth, int nVars );
diff --git a/src/misc/extra/extraUtilTruth.c b/src/misc/extra/extraUtilTruth.c
index ab476f6f..7a22545b 100644
--- a/src/misc/extra/extraUtilTruth.c
+++ b/src/misc/extra/extraUtilTruth.c
@@ -250,64 +250,6 @@ void Extra_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll
 
 /**Function*************************************************************
 
-  Synopsis    [Performs truth table computation.]
-
-  Description [Note the caching makes no sense for this procedure.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Extra_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal )
-{
-    DdNode * bF0, * bF1, * bF;
-    if ( nVars == 0 )
-    {
-        if ( pTruth[iBit>>5] & (1 << iBit&31) )
-            return b1;
-        return b0;
-    }
-    if ( nVars == 5 )
-    {
-        if ( pTruth[iBit>>5] == 0xFFFFFFFF )
-            return b1;
-        if ( pTruth[iBit>>5] == 0 )
-            return b0;
-    }
-    // other special cases can be added
-    bF0 = Extra_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal );  Cudd_Ref( bF0 );
-    bF1 = Extra_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal );  Cudd_Ref( bF1 );
-    bF  = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 );                       Cudd_Ref( bF );
-    Cudd_RecursiveDeref( dd, bF0 );
-    Cudd_RecursiveDeref( dd, bF1 );
-    Cudd_Deref( bF );
-    return bF;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compute BDD corresponding to the truth table.]
-
-  Description [If truth table has N vars, the BDD depends on N topmost
-  variables of the BDD manager. The most significant variable of the table
-  is encoded by the topmost variable of the manager. BDD construction is 
-  very efficient in this case because BDD is constructed one node at a time, 
-  by simply adding BDD nodes on top of existent BDD nodes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Extra_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars )
-{
-    return Extra_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars );
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Returns 1 if TT depends on the given variable.]
 
   Description []
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 1973bd46..10918156 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -598,6 +598,9 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
 ***********************************************************************/
 static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
 {
+    if ( nWords == 0 )
+        return NULL;
+    assert( nWords > 0 );
     p->nSize += nWords;
     if ( p->nSize > p->nCap )
     {