diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index bb3c6524d..eec6dd226 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -853,7 +853,9 @@ extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern void                Gia_ManVerifyChoices( Gia_Man_t * p );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
+extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 3c5ad848b..492f55ef0 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -53,7 +53,7 @@ int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
         return 0;
     if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
         return 0;
-    pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+    pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL;
     return pRepr == NULL || pRepr->Value == 0;
 }
 
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index e56f6ea92..333fe58e7 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -961,6 +961,41 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManVerifyChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, fProb = 0;
+    assert( p->pReprs );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
+                printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
+                printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
+                printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
+        }
+    }
+    if ( !fProb )
+        printf( "GIA with choices is correct.\n" );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if AIG has dangling nodes.]
@@ -993,6 +1028,37 @@ int Gia_ManHasDangling( Gia_Man_t * p )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has dangling nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManMarkDangling( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        Counter += !pObj->fMark0;
+    return Counter;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if AIG has dangling nodes.]