diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 24c1d3b0e..9d9b56a1c 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -5703,8 +5703,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
         pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
 
     // TODO: record the corresponding impl node of each lit
-    vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) );
-    Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 );
+    vLitBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2 );
+    Vec_IntFill( vLitBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2, 0 );
+    printf( "allocated size: %d\n", Vec_IntSize(vLitBmiter) );
 
     Gia_ManForEachAnd( p2, pObj, i )
     {
@@ -5776,7 +5777,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
 
     Gia_ManStaticFanoutStop( p1 );
 
-    printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) );
+    printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) );
 
 
     // TODO: record hashed equivalent nodes
@@ -5798,17 +5799,30 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
             Vec_IntPush( vLits, pObj->Value );
     }
 
-    // int e;
-    // Vec_IntForEachEntry( vLitBmiter, e, i )
-    // {
-    //     printf( "%d ", e );
-    // }
-    // printf("\n");
+
+    int e, c3=0, c4=0, c5=0;
+    c1 = 0; c2 = 0;
+
+    Vec_IntForEachEntry( vLitBmiter, e, i )
+    {
+        if ( i%2 ) continue;
+        switch (e)
+        {
+        case 1: c1++; break;
+        case 2: c2++; break;
+        case 3: c3++; break;
+        case 4: c4++; break;
+        case 5: c5++; break;
+        default:
+            break;
+        }
+    }
+    printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
 
     Gia_ManForEachCo( p2, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    //Gia_ManForEachCo( p1, pObj, i )
-    //    Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachCo( p1, pObj, i )
+       Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Vec_IntForEachEntry( vLits, iLit, i )
         Gia_ManAppendCo( pNew, iLit );
     Vec_IntFree( vLits );
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 424369b8c..4a39e95d3 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1882,8 +1882,46 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
             if ( pRepr == NULL )
                 continue;
         }
+        int lit_obj = Gia_ObjId( p, pObj ) << 1;
+        int lit_repr = Gia_ObjId( p, pRepr ) << 1;
+
         if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
         {
+            // printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) );
+            if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
+            {
+                switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
+                {
+                    case 1:
+                    case 4:
+                        Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
+                        break;
+                    case 2:
+                    case 5:
+                        Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
+                        break;
+                    default:
+                        break;
+                }
+            }
+            else 
+            {
+                if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) 
+                    switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
+                    {
+                        case 1:
+                        case 4:
+                            Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
+                            break;
+                        case 2:
+                        case 5:
+                            Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
+                            break;
+                        default:
+                            break;
+
+                    }
+            }
             assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
             Gia_ObjSetProved( p, i );
             if ( Gia_ObjId(p, pRepr) == 0 )
@@ -1893,17 +1931,18 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
         if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
         {
             if (pPars->fBMiterInfo){
-                if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 )
+                // printf( "node %d (%d) merged into node %d (%d)\n", lit_obj, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr, Vec_IntEntry( vLitBmiter, lit_repr ) );
+                if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
                 {
-                    switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) )
+                    switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
                     {
                         case 1:
                         case 4:
-                            Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 );
+                            Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
                             break;
                         case 2:
                         case 5:
-                            Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 );
+                            Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
                             break;
                         default:
                             break;
@@ -1911,16 +1950,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
                 }
                 else 
                 {
-                    if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) 
-                        switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) )
+                    if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) 
+                        switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
                         {
                             case 1:
                             case 4:
-                                Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 );
+                                Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
                                 break;
                             case 2:
                             case 5:
-                                Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 );
+                                Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
                                 break;
                             default:
                                 break;
@@ -1998,7 +2037,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
                 break;
             }
         }
-        printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5);
+        printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
     }
     return pNew;
 }