From 9f4ab5a2c1612400b1c9ebf95573a7d8bdf8b5db Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 22 Apr 2023 18:37:21 -0700
Subject: [PATCH] Bug fix in SAT sweeping.

---
 src/aig/gia/giaEquiv.c   | 2 +-
 src/proof/cec/cecSatG2.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 030eaa60d..1c3aa4311 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -528,7 +528,7 @@ int Gia_ManChoiceMinLevel_rec( Gia_Man_t * p, int iPivot, int fDiveIn, Vec_Int_t
 {
     int Level0, Level1, LevelMax;
     Gia_Obj_t * pPivot = Gia_ManObj( p, iPivot );
-    if ( Gia_ObjIsCi(pPivot) )
+    if ( Gia_ObjIsCi(pPivot) || iPivot == 0 )
         return 0;
     if ( Gia_ObjLevel(p, pPivot) )
         return Gia_ObjLevel(p, pPivot);
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 4e21da404..ef93548bd 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1864,7 +1864,7 @@ finalize:
     Cec4_ManDestroy( pMan );
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
-    if ( *ppNew == NULL )
+    if ( ppNew && *ppNew == NULL )
         *ppNew = Gia_ManDup(p);
     return p->pCexSeq ? 0 : 1;
 }