diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index c95492e28..9cbbe3cad 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -2053,7 +2053,7 @@ finalize:
     //Gia_ManEquivPrintClasses( p, 1, 0 );
     if ( ppNew && *ppNew == NULL )
         *ppNew = Gia_ManDup(p);
-    Gia_ManRemoveWrongChoices( p );
+    if ( p->pNexts ) Gia_ManRemoveWrongChoices( p );
     return p->pCexSeq ? 0 : 1;
 }
 Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
diff --git a/src/proof/cec/cecSatG3.c b/src/proof/cec/cecSatG3.c
index 58696310b..133bf4a90 100644
--- a/src/proof/cec/cecSatG3.c
+++ b/src/proof/cec/cecSatG3.c
@@ -2120,7 +2120,7 @@ finalize:
         CbsP_ManStop(pCbs);
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
-    Gia_ManRemoveWrongChoices( p );
+    if ( p->pNexts ) Gia_ManRemoveWrongChoices( p );
     return p->pCexSeq ? 0 : 1;
 }
 Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle )