diff --git a/src/aig/gia/giaSif.c b/src/aig/gia/giaSif.c
index e5ba96a39..db7629fb3 100644
--- a/src/aig/gia/giaSif.c
+++ b/src/aig/gia/giaSif.c
@@ -359,7 +359,7 @@ Vec_Int_t * Gia_ManSifTimesToCounts( Gia_Man_t * p, Vec_Int_t * vTimes, int Peri
 }
 Gia_Man_t * Gia_ManSifTransform( Gia_Man_t * p, Vec_Int_t * vCuts, Vec_Int_t * vTimes, int nLutSize, int Period, int fVerbose )
 {
-    Gia_Man_t * pTemp = NULL, * pNew = NULL; Vec_Int_t * vCounts = NULL, * vTimesNew = NULL;
+    Gia_Man_t * pNew = NULL; Vec_Int_t * vCounts = NULL;
     if ( fVerbose )
         printf( "Current area = %d.  Period = %d.  ", Gia_ManSifArea(p, vCuts, nLutSize+1), Period );
     if ( fVerbose )
diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index f9fede188..aa16771ef 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -1217,6 +1217,36 @@ static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize )
     return (Vec_Wrd_t *)vResInt;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of common entries.]
+
+  Description [Assumes that the vectors are sorted in the increasing order.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_WrdTwoCountCommon( Vec_Wrd_t * vArr1, Vec_Wrd_t * vArr2 )
+{
+    word * pBeg1 = vArr1->pArray;
+    word * pBeg2 = vArr2->pArray;
+    word * pEnd1 = vArr1->pArray + vArr1->nSize;
+    word * pEnd2 = vArr2->pArray + vArr2->nSize;
+    int Counter = 0;
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            pBeg1++, pBeg2++, Counter++;
+        else if ( *pBeg1 < *pBeg2 )
+            pBeg1++;
+        else
+            pBeg2++;
+    }
+    return Counter;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Comparison procedure for two integers.]
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 9c67a51bf..4e21da404 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1864,6 +1864,8 @@ finalize:
     Cec4_ManDestroy( pMan );
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
+    if ( *ppNew == NULL )
+        *ppNew = Gia_ManDup(p);
     return p->pCexSeq ? 0 : 1;
 }
 Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )