From 7884dd01bc07b4f052436f996eee3cb66169a556 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 1 Oct 2011 10:50:50 +0700
Subject: Fixed a corner case bug in dprove when a trivial CEX is not produced.

---
 src/aig/fra/fraSec.c | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src')

diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index ca8cf799..3b28936d 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -620,6 +620,17 @@ ABC_PRT( "Time", clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
+        if ( pNew->pSeqModel == NULL )
+        {
+            int i;
+            // if the CEX is not derives, it is because tricial CEX should be assumed
+            pNew->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pNew), pNew->nTruePis, 1 );
+            // if the CEX does not work, we need to change PIs to 1 because 
+            // the only way it can happen is when a PO is equal to a PI...
+            if ( Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ) == -1 )
+                for ( i = 0; i < pNew->nTruePis; i++ )
+                    Aig_InfoSetBit( pNew->pSeqModel->pData, i );
+        }
         if ( !pParSec->fSilent )
         {
             printf( "Networks are NOT EQUIVALENT.   " );
-- 
cgit v1.2.3