Experimental code for polynomial construction.

src/base/exor/exor.c

@@ -78,6 +78,7 @@ extern int s_fDecreaseLiterals;
   SeeAlso     []
 
 ***********************************************************************/
+/*
 static int QCost[16][16] = 
 {
     {  1}, // 0
@@ -90,6 +91,7 @@ static int QCost[16][16] =
     { 56,  56,  56,  56,  58,  60,  62,  64}, // 7
     { 0 }
 };
+*/
 int GetQCost( int nVars, int nNegs )
 {
     int Extra;

src/proof/acec/acecCo.c

@@ -93,7 +93,7 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t *
     Vec_Int_t * vRoots  = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) );
     Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) );
     Vec_Wec_t * vMap    = Vec_WecStart( Gia_ManObjNum(pGia) );
-    int i, k, Index, Driver, Entry1, Entry2;
+    int i, k, Index, Driver, Entry1, Entry2 = -1;
     // nodes driven by adders into adder indexes
     for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
     {

src/proof/acec/acecPo.c

@@ -339,7 +339,6 @@ Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int
     // complement leave nodes
     Vec_IntForEachEntry( vLeaves, iObj, i )
     {
-        Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj );
         int iLits[2] = { Abc_Var2Lit(iObj, 0),  Abc_Var2Lit(iObj, 1) };
         // add inverter
         Vec_Int_t * vArray = Vec_WecEntry( vLit2Mono, iLits[1] );