From 265db2a9d147417dc845445dbf28461ed0c5c621 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 13 May 2011 10:19:29 +0800
Subject: Fixing mismatch in reconcile.

---
 src/aig/llb/llb4Cex.c | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'src/aig/llb')

diff --git a/src/aig/llb/llb4Cex.c b/src/aig/llb/llb4Cex.c
index 42515a77..6c4cedfb 100644
--- a/src/aig/llb/llb4Cex.c
+++ b/src/aig/llb/llb4Cex.c
@@ -237,7 +237,17 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
     }
 */
     assert( iBit == p->nBits );
-    if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+//    if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+//        Vec_PtrFreeP( &vStates );
+    for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- )
+    {
+        if ( Aig_ManPo(pAig, i)->fMarkB )
+        {
+            p->iPo = i;
+            break;
+        }
+    }
+    if ( i == -1 )
         Vec_PtrFreeP( &vStates );
     Aig_ManCleanMarkB(pAig);
     return vStates;
-- 
cgit v1.2.3