From f04f9c43531596c04230e0dfa6a119b92fd9ab48 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 8 May 2024 23:45:14 -0700
Subject: [PATCH] Updating counter-example generation.

---
 src/aig/gia/giaPat2.c | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
index b45634ed8..b557ac6f8 100644
--- a/src/aig/gia/giaPat2.c
+++ b/src/aig/gia/giaPat2.c
@@ -1384,15 +1384,18 @@ void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCe
     int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
     Gia_ManForEachCo( p, pObj, i ) {
         if ( Gia_ObjFaninLit0p(p, Gia_ManCo(p, i)) == 0 ) {
-            fprintf( pFile, "%d :\n", i );
+            fprintf( pFile, "%d : unsat\n", i );
             nOuts[0]++;
         }
         else if ( fShort ) {
             for ( c = 0; c < nCexes; c++ ) {
                 Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
                 fprintf( pFile, "%d :", i );
-                Vec_IntForEachEntry( vPat, iLit, k )
-                    fprintf( pFile, " %d", iLit );
+                if ( Vec_IntSize(vPat) == 0 )
+                    fprintf( pFile, " not available" );
+                else
+                    Vec_IntForEachEntry( vPat, iLit, k )
+                        fprintf( pFile, " %d", iLit );
                 fprintf( pFile, "\n" );
             }
             nOuts[1]++;