From 93b96fc35c50123eb48b04d212394036dd8a8109 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 6 Dec 2017 14:34:03 -0800
Subject: An improvement to 'twoexact' and 'lutexact'.

---
 src/sat/bmc/bmcMaj2.c | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/sat/bmc/bmcMaj2.c')

diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
index 54745118..a3c1027a 100644
--- a/src/sat/bmc/bmcMaj2.c
+++ b/src/sat/bmc/bmcMaj2.c
@@ -553,7 +553,11 @@ static int Exa_ManMarkup( Exa_Man_t * p )
                 continue;
             }
 #endif
+#ifdef USE_LESS_VARS
             for ( j = 1 - k; j < i - k; j++ )
+#else
+            for ( j = 0; j < i - k; j++ )
+#endif
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
@@ -936,7 +940,11 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
                 continue;
             }
 #endif
+#ifdef USE_LESS_VARS
             for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
+#else
+            for ( j = 0; j < i - k; j++ )
+#endif
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
-- 
cgit v1.2.3