summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcMaj.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc/bmcMaj.c')
-rw-r--r--src/sat/bmc/bmcMaj.c4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 86934898..97322eae 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -438,6 +438,7 @@ int Exa_ManMarkup( Exa_Man_t * p )
{
for ( k = 0; k < 2; k++ )
{
+#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@@ -445,6 +446,7 @@ int Exa_ManMarkup( Exa_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
+#endif
for ( j = 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
@@ -817,6 +819,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
{
for ( k = 0; k < p->nLutSize; k++ )
{
+#ifdef USE_FIRST_SPECIAL
if ( i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
@@ -824,6 +827,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
+#endif
for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );