From 8cde0dd33c00fb9525e835551f87a1525ad70f3b Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 31 Aug 2011 11:37:59 +0700
Subject: Bug fix in CBA.

---
 src/aig/saig/saigAbsCba.c | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src')

diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index f79cbf09..4d9cef57 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -621,6 +621,11 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
         assert( pAbs->pSeqModel == NULL );
         return Vec_IntAlloc( 0 );
     }
+    if ( pAbs->pSeqModel == NULL )
+    {
+        printf( "BMC did not detect a CEX with the given depth.\n" );
+        return Vec_IntAlloc( 0 );
+    }
     if ( pPars->fVerbose )
         Abc_CexPrintStats( pAbs->pSeqModel );
     // CEX is detected - refine the flops
-- 
cgit v1.2.3