From 3552d39b7193be6e1c740b7a6b2c80225d9726be Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 24 Feb 2012 13:37:31 -0800
Subject: Making BMC engines (bmc2, bmc3) to perform OR-decomposition by
 default.

---
 src/base/abci/abcDar.c | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 8efa669f..8797b167 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -133,10 +133,17 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
     // collect the drivers
     vSuper   = Vec_PtrAlloc( 100 );
     vDrivers = Vec_PtrAlloc( 100 );
-    if ( pvMap )
+    if ( pvMap ) 
     *pvMap   = Vec_IntAlloc( 100 );
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
+        if ( pNtk->nConstrs && i >= pNtk->nConstrs )
+        {
+            Vec_PtrPush( vDrivers, Abc_ObjNot(Abc_ObjChild0(pObj)) );
+            if ( pvMap )
+            Vec_IntPush( *pvMap, i );
+            continue;
+        }
         Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
         Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
         {
-- 
cgit v1.2.3