diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index e513861fe..b82f35777 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -1340,7 +1340,21 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
         printf( " )\n" );
     }
 }
-
+static void Exa3_ManPrintPerm( Exa3_Man_t * p )
+{
+    int i, k, iVar;
+    for ( i = p->nVars; i < p->nObjs; i++ )
+    {
+        if ( i > p->nVars )
+            printf( "_" );
+        for ( k = p->nLutSize - 1; k >= 0; k-- )
+        {
+            iVar = Exa3_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                printf( "%c", 'a'+iVar );
+        }
+    }
+}
 /**Function*************************************************************
 
   Synopsis    []
@@ -1678,8 +1692,12 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     }
     if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
         Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
-    if ( iMint == -1 )
+    if ( iMint == -1 ) {
         Exa3_ManPrintSolution( p, fCompl ), Res = 1;
+        printf( "The variable permutation is \"" );
+        Exa3_ManPrintPerm(p);
+        printf( "\".\n" );
+    }
     else if ( status == GLUCOSE_UNDEC )
         printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
     else if ( !p->pPars->fSilent ) 
diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c
index 17073c1d1..902c5006a 100644
--- a/src/sat/bmc/bmcMaj8.c
+++ b/src/sat/bmc/bmcMaj8.c
@@ -419,6 +419,21 @@ static void Exa8_ManPrintSolution( Exa8_Man_t * p, int fCompl )
         printf( " )\n" );
     }
 }
+static void Exa8_ManPrintPerm( Exa8_Man_t * p )
+{
+    int i, k, iVar;
+    for ( i = p->nVars; i < p->nObjs; i++ )
+    {
+        if ( i > p->nVars )
+            printf( "_" );
+        for ( k = p->nLutSize - 1; k >= 0; k-- )
+        {
+            iVar = Exa8_ManFindFanin( p, i, k );
+            if ( iVar >= 0 && iVar < p->nVars )
+                printf( "%c", 'a'+iVar );
+        }
+    }
+}
 
 /**Function*************************************************************
 
@@ -714,6 +729,9 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
         if ( DiffMint != -1 )
             printf( "Warning: Verification detected a mismatch at minterm %d.\n", DiffMint );
         Exa8_ManPrintSolution( p, fCompl );
+        printf( "The variable permutation is \"" );
+        Exa8_ManPrintPerm(p);
+        printf( "\".\n" );
         if ( pPars->fDumpBlif )
             Exa8_ManDumpBlif( p, fCompl );
         Res = 1;