diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 682ca67a6..f74581834 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -51574,7 +51574,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
     Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
-    char * pReplayFile = NULL, * pUfarArgs = NULL;
+    char * pReplayFile = NULL, * pUfarArgs = NULL, * pUfarArgsAlloc = NULL;
     int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "PTUCWRusvwh" ) ) != EOF )
@@ -51621,8 +51621,22 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-C\" should be followed by a string.\n" );
                 goto usage;
             }
-            pUfarArgs = argv[globalUtilOptind];
-            globalUtilOptind++;
+            {
+                int iArg, nChars = 0;
+                ABC_FREE( pUfarArgsAlloc );
+                for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
+                    nChars += (int)strlen(argv[iArg]) + 1;
+                pUfarArgsAlloc = ABC_ALLOC( char, nChars + 1 );
+                pUfarArgsAlloc[0] = 0;
+                for ( iArg = globalUtilOptind; iArg < argc; iArg++ )
+                {
+                    if ( iArg > globalUtilOptind )
+                        strcat( pUfarArgsAlloc, " " );
+                    strcat( pUfarArgsAlloc, argv[iArg] );
+                }
+                pUfarArgs = pUfarArgsAlloc;
+                globalUtilOptind = argc;
+            }
             break;
         case 'W':
             if ( globalUtilOptind >= argc )
@@ -51668,18 +51682,21 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pWlc == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no word-level design for option \"-u\".\n" );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL );
         if ( pGiaTemp == NULL )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): Word-level bit-blasting has failed.\n" );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 )
         {
             Abc_Print( -1, "Abc_CommandAbc9SProve(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" );
             Gia_ManStop( pGiaTemp );
+            ABC_FREE( pUfarArgsAlloc );
             return 1;
         }
         pGiaUse = Gia_ManTransformMiter2( pGiaTemp );
@@ -51689,11 +51706,13 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     else if ( pUfarArgs != NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9SProve(): Option \"-C\" requires \"-u\".\n" );
+        ABC_FREE( pUfarArgsAlloc );
         return 1;
     }
     if ( pGiaUse == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
+        ABC_FREE( pUfarArgsAlloc );
         return 1;
     }
     if ( Gia_ManRegNum(pGiaUse) == 0 )
@@ -51701,12 +51720,14 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" );
         if ( fUseUif )
             Gia_ManStop( pGiaUse );
+        ABC_FREE( pUfarArgsAlloc );
         return 1;
     }
     pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile, pUfarArgs );
     Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); 
     if ( fUseUif )
         Gia_ManStop( pGiaUse );
+    ABC_FREE( pUfarArgsAlloc );
     return 0;
 
 usage:
@@ -51723,6 +51744,7 @@ usage:
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing more verbose information [default = %s]\n",    fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
+    ABC_FREE( pUfarArgsAlloc );
     return 1;
 }
 
diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp
index c3f64d2b1..6270cbb59 100755
--- a/src/opt/ufar/UfarCmd.cpp
+++ b/src/opt/ufar/UfarCmd.cpp
@@ -311,6 +311,104 @@ static bool Ufar_TokenizeArgs( const char * pArgs, vector<string> & Tokens )
     return true;
 }
 
+static inline void Ufar_TrimString( string & s )
+{
+    while ( !s.empty() && isspace((unsigned char)s.front()) )
+        s.erase( s.begin() );
+    while ( !s.empty() && isspace((unsigned char)s.back()) )
+        s.pop_back();
+}
+
+static bool Ufar_ExtractSolverArg( const char * pArgs, string & ArgsWithoutSolver, string & SolverArg )
+{
+    string Args = pArgs ? pArgs : "";
+    size_t i = 0, n = Args.size();
+    ArgsWithoutSolver = Args;
+    SolverArg.clear();
+    while ( i < n )
+    {
+        while ( i < n && isspace((unsigned char)Args[i]) )
+            i++;
+        if ( i == n )
+            break;
+        size_t TokenStart = i;
+        char Quote = 0;
+        string Token;
+        while ( i < n )
+        {
+            unsigned char c = (unsigned char)Args[i];
+            if ( Quote )
+            {
+                if ( c == (unsigned char)Quote )
+                    Quote = 0;
+                else if ( c == '\\' && i + 1 < n )
+                    Token += Args[++i];
+                else
+                    Token += (char)c;
+                i++;
+                continue;
+            }
+            if ( c == '"' || c == '\'' )
+            {
+                Quote = (char)c;
+                i++;
+                continue;
+            }
+            if ( isspace(c) )
+                break;
+            if ( c == '\\' && i + 1 < n )
+            {
+                Token += Args[++i];
+                i++;
+                continue;
+            }
+            Token += (char)c;
+            i++;
+        }
+        if ( Token == "--solver" )
+        {
+            size_t ValueStart = i;
+            while ( ValueStart < n && isspace((unsigned char)Args[ValueStart]) )
+                ValueStart++;
+            if ( ValueStart == n )
+                return false;
+            string Prefix = Args.substr( 0, TokenStart );
+            string Suffix;
+            if ( Args[ValueStart] == '"' || Args[ValueStart] == '\'' )
+            {
+                char ValueQuote = Args[ValueStart++];
+                size_t k = ValueStart;
+                while ( k < n )
+                {
+                    unsigned char c = (unsigned char)Args[k];
+                    if ( c == (unsigned char)ValueQuote )
+                    {
+                        k++;
+                        break;
+                    }
+                    if ( c == '\\' && k + 1 < n )
+                        SolverArg += Args[++k];
+                    else
+                        SolverArg += (char)c;
+                    k++;
+                }
+                Suffix = Args.substr( k );
+            }
+            else
+            {
+                SolverArg = Args.substr( ValueStart );
+            }
+            Ufar_TrimString( SolverArg );
+            ArgsWithoutSolver = Prefix + Suffix;
+            Ufar_TrimString( ArgsWithoutSolver );
+            return !SolverArg.empty();
+        }
+        while ( i < n && isspace((unsigned char)Args[i]) )
+            i++;
+    }
+    return false;
+}
+
 
 void Ufar_Init(Abc_Frame_t *pAbc)
 {
@@ -328,6 +426,7 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
     vector<string> Tokens;
     vector<char *> Argv;
     set<unsigned> set_op_types;
+    string ArgsWithoutSolver, SolverArg;
     string firstAigDumpFile, dumpLogFile;
     string statusName;
     int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
@@ -338,9 +437,12 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
     Ufar_SetDefaultParams( manager.params, nTimeOut, fVerbose, pFuncStop, RunId );
     if ( pArgs && pArgs[0] )
     {
+        const char * pParseArgs = pArgs;
+        if ( Ufar_ExtractSolverArg(pArgs, ArgsWithoutSolver, SolverArg) )
+            pParseArgs = ArgsWithoutSolver.c_str();
         OptMgr opt_mgr("%ufar");
         Ufar_AddOptions( opt_mgr, manager.params );
-        if ( !Ufar_TokenizeArgs(pArgs, Tokens) )
+        if ( !Ufar_TokenizeArgs(pParseArgs, Tokens) )
         {
             cout << "Cannot parse internal %ufar option string." << endl;
             return -1;
@@ -355,6 +457,8 @@ int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*p
             return -1;
         }
         Ufar_ApplyOptions( opt_mgr, manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
+        if ( !SolverArg.empty() )
+            manager.params.solverSetting = SolverArg;
     }
     else
         set_op_types.insert( WLC_OBJ_ARI_MULTI );