From 4efc89d3421198005af1b6a5971809628897aa19 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 23 Jan 2013 16:50:45 +0700
Subject: Enabled detecting CEXes in multiple POs without stopping (sim3 -a).

---
 src/proof/ssw/sswRarity.c | 52 ++++++++++++++++++++++-------------------------
 1 file changed, 24 insertions(+), 28 deletions(-)

(limited to 'src/proof')

diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index da96d218..d2c6451e 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -549,44 +549,40 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
 int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
 {
     Aig_Obj_t * pObj;
-    int i;
+    int i, RetValue = 0;
     p->iFailPo  = -1;
     p->iFailPat = -1;
     Saig_ManForEachPo( p->pAig, pObj, i )
     {
         if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
-            return 0;
+            break;
         if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
             continue;
-        if ( !Ssw_RarManObjIsConst(p, pObj) )
+        if ( Ssw_RarManObjIsConst(p, pObj) )
+            continue;
+        RetValue = 1;
+        p->iFailPo  = i;
+        p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
+        if ( pnSolvedNow == NULL )
+            break;
+        // remember the one solved
+        (*pnSolvedNow)++;
+        if ( p->vCexes == NULL )
+            p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
+        assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
+        Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
+        // print final report
+        if ( !fNotVerbose )
         {
-            p->iFailPo  = i;
-            p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
-
-            // remember the one solved
-            if ( pnSolvedNow )
-            {
-                (*pnSolvedNow)++;
-                if ( p->vCexes == NULL )
-                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
-                assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
-                Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
-                // print final report
-                if ( !fNotVerbose )
-                {
-                    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
-                    Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs).  ", 
-                        nOutDigits, p->iFailPo, iFrame, 
-                        nOutDigits, *pnSolvedNow, 
-                        nOutDigits, Saig_ManPoNum(p->pAig) );
-                    Abc_PrintTime( 1, "Time", Time );
-                }
-                continue;
-            }
-            return 1;
+            int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
+            Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs).  ", 
+                nOutDigits, p->iFailPo, iFrame, 
+                nOutDigits, *pnSolvedNow, 
+                nOutDigits, Saig_ManPoNum(p->pAig) );
+            Abc_PrintTime( 1, "Time", Time );
         }
     }
-    return 0;
+    return RetValue;
 }
 
 /**Function*************************************************************
-- 
cgit v1.2.3