From 8c9e66205e9ae7e05e48e723132270fbb0564fef Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 11 May 2026 13:49:26 -0700
Subject: [PATCH] Bug fix in &sprove.

---
 src/proof/abs/absGla.c | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 9f1a8a31e..72863fe73 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1847,7 +1847,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         }
     }
 finish:
-    Prf_ManStopP( &p->pSat->pPrf2 );
+    if ( p->pSat )
+        Prf_ManStopP( &p->pSat->pPrf2 );
     // cancel old one if it is proving
     if ( iFrameTryToProve >= 0 )
         Gia_GlaProveCancel( pPars->fVerbose );
@@ -1860,9 +1861,9 @@ finish:
     {
         Vec_IntFreeP( &pAig->vGateClasses );
         pAig->vGateClasses = Ga2_ManAbsTranslate( p );
-        if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
+        if ( p->pSat && p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
             Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
-        else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
+        else if ( p->pSat && pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
             Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
         else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
             Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement.  ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
@@ -1893,7 +1894,8 @@ finish:
         ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
         ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
         ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
-        Ga2_ManReportMemory( p );
+        if ( p->pSat )
+            Ga2_ManReportMemory( p );
     }
 //    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
     Ga2_ManStop( p );