diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d638a6898..899058545 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10826,11 +10826,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Truth table should be given on the command line.\n" );
         return 1;
     }
+    if ( pPars->nVars == 0 && pPars->pTtStr )
+        pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr));
     if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
     {
         Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
         return 1;
     }
+    if ( pPars->nVars == 0 && pPars->pSymStr )
+        pPars->nVars = (int)strlen(pPars->pSymStr) - 1;
     if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) )
     {
         Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) );
@@ -10843,7 +10847,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pPars->nVars > 12 )
     {
-        Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
+        Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
         return 1;
     }
     if ( pPars->nLutSize > 6 )
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 780271c47..ddb3be453 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -1291,7 +1291,7 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
     {
         int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
-        printf( "%02d = %d\'b", i, 1 << p->nLutSize );
+        printf( "%c = %d\'b", 'A'+i-p->nVars, 1 << p->nLutSize );
         for ( k = p->LutMask - 1; k >= 0; k-- )
         {
             Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k); 
@@ -1311,7 +1311,7 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
             if ( iVar >= 0 && iVar < p->nVars )
                 printf( " %c", 'a'+iVar );
             else
-                printf( " %02d", iVar );
+                printf( " %c", 'A'+iVar-p->nVars );
         }
         printf( " )\n" );
     }
@@ -1332,7 +1332,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
 {
     int i, k, b, iVar;
     char pFileName[1000];
-    char * pStr = Abc_UtilStrsav(p->pPars->pTtStr);
+    char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr);
     if ( strlen(pStr) > 16 ) {
         pStr[16] = '_';
         pStr[17] = '\0';