diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 998b3e16b..691842fc8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -686,7 +686,7 @@ extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wr
 typedef struct Wlc_Ntk_t_    Wlc_Ntk_t;
 typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
 extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
-extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile );
+extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs );
 extern int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif );
 extern int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent );
 
@@ -51559,10 +51559,10 @@ 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;
+    char * pReplayFile = NULL, * pUfarArgs = 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, "PTUWRusvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PTUCWRusvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -51599,7 +51599,16 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             if ( nTimeOut2 <= 0 )
                 goto usage;
-            break;    
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pUfarArgs = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
         case 'W':
             if ( globalUtilOptind >= argc )
             {
@@ -51662,6 +51671,11 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Gia_ManStop( pGiaTemp );
         pGiaTemp = NULL;
     }
+    else if ( pUfarArgs != NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SProve(): Option \"-C\" requires \"-u\".\n" );
+        return 1;
+    }
     if ( pGiaUse == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
@@ -51674,18 +51688,19 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             Gia_ManStop( pGiaUse );
         return 1;
     }
-    pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    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 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sprove [-PTUW num] [-R file] [-usvwh]\n" );
+    Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" );
     Abc_Print( -2, "\t         proves CEC problem by case-splitting\n" );
     Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs );
     Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut );
-    Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut2 );
+    Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 );
+    Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" );
     Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut3 );
     Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" );
     Abc_Print( -2, "\t-u     : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" );
diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp
index f4bd70b20..50b631a54 100755
--- a/src/opt/ufar/UfarCmd.cpp
+++ b/src/opt/ufar/UfarCmd.cpp
@@ -17,6 +17,7 @@
 #include <regex>
 #include <cstdlib>
 #include <cstdio>
+#include <cctype>
 
 #include "base/wlc/wlc.h"
 #include "aig/gia/giaAig.h"
@@ -30,6 +31,14 @@ ABC_NAMESPACE_IMPL_START
 using namespace std;
 
 static UFAR::UfarManager ufar_manager;
+typedef struct Ufar_StopCtx_t_
+{
+    int (*pFuncStop)(int);
+    int nTimeOut;
+    int fActive;
+    timeval TimeStart;
+} Ufar_StopCtx_t;
+static __thread Ufar_StopCtx_t g_UfarStopCtx = { NULL, 0, 0, {0, 0} };
 
 static int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAnalyzeCex( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -40,6 +49,38 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
+static inline long long   Ufar_ElapsedUsec( const timeval & Start, const timeval & Stop ) { return 1000000ll * (long long)(Stop.tv_sec - Start.tv_sec) + (long long)(Stop.tv_usec - Start.tv_usec); }
+
+static int Ufar_StopWithTimeout( int RunId )
+{
+    if ( g_UfarStopCtx.pFuncStop && g_UfarStopCtx.pFuncStop(RunId) )
+        return 1;
+    if ( g_UfarStopCtx.fActive && g_UfarStopCtx.nTimeOut > 0 )
+    {
+        timeval Now;
+        gettimeofday( &Now, NULL );
+        if ( Ufar_ElapsedUsec(g_UfarStopCtx.TimeStart, Now) >= 1000000ll * (long long)g_UfarStopCtx.nTimeOut )
+            return 1;
+    }
+    return 0;
+}
+
+struct Ufar_StopScope_t
+{
+    Ufar_StopCtx_t Saved;
+    Ufar_StopScope_t( int (*pFuncStop)(int), int nTimeOut )
+    {
+        Saved = g_UfarStopCtx;
+        g_UfarStopCtx.pFuncStop = pFuncStop;
+        g_UfarStopCtx.nTimeOut = nTimeOut;
+        g_UfarStopCtx.fActive = 1;
+        gettimeofday( &g_UfarStopCtx.TimeStart, NULL );
+    }
+    ~Ufar_StopScope_t()
+    {
+        g_UfarStopCtx = Saved;
+    }
+};
 
 static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk )
 {
@@ -74,6 +115,194 @@ static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const str
     fclose( pFile );
 }
 
+static void Ufar_SetDefaultParams( UFAR::UfarManager::Params & Params, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
+{
+    Params = UFAR::UfarManager::Params();
+    Params.RunId = RunId;
+    Params.pFuncStop = pFuncStop;
+    if ( nTimeOut > 0 )
+        Params.nTimeout = nTimeOut;
+    Params.iVerbosity = fVerbose ? 1 : 0;
+}
+static void Ufar_AddOptions( OptMgr & opt_mgr, const UFAR::UfarManager::Params & Params )
+{
+    opt_mgr.AddOpt("--norm", Params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
+    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
+    opt_mgr.AddOpt("--cexmin", Params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
+    opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
+    opt_mgr.AddOpt("-v", to_string(Params.iVerbosity), "num", "specify verbosity level");
+    opt_mgr.AddOpt("--seq", to_string(Params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
+    opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
+    opt_mgr.AddOpt("--pba_uif", Params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
+    opt_mgr.AddOpt("--lazysim", Params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
+    opt_mgr.AddOpt("--pbasim", Params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
+    opt_mgr.AddOpt("--pbacex", Params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
+    opt_mgr.AddOpt("--satmin", Params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
+    opt_mgr.AddOpt("--cbawb", Params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
+    opt_mgr.AddOpt("--grey", Params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
+    opt_mgr.AddOpt("--grey2", to_string(Params.nGrey), "float", "specify the greyness threshold");
+    opt_mgr.AddOpt("--allwb", Params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
+    opt_mgr.AddOpt("--crossonly", Params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
+    opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
+    opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
+    opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
+    opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
+    opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
+    opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
+    opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
+    opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
+    opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
+    opt_mgr.AddOpt("--sp", Params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
+    opt_mgr.AddOpt("--simp", Params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
+    opt_mgr.AddOpt("--syn", Params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
+    opt_mgr.AddOpt("--pth", Params.fPthread ? "yes" : "no", "", "toggle using pthreads");
+    opt_mgr.AddOpt("--onewb", to_string(Params.iOneWb), "int", "specify the mode for one-white-boxing");
+    opt_mgr.AddOpt("--initallpairs", to_string(Params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
+    opt_mgr.AddOpt("--initnear", to_string(Params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
+    opt_mgr.AddOpt("--timeout", to_string(Params.nTimeout), "num", "specify the timeout (sec)");
+    opt_mgr.AddOpt("--exp", to_string(Params.iExp), "int", "specify the exp mode");
+    opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
+    opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
+}
+static void Ufar_ApplyOptions( OptMgr & opt_mgr, UFAR::UfarManager::Params & Params, set<unsigned> & set_op_types, string & firstAigDumpFile, string & dumpLogFile, int & fNeedMiter, int & fCrossStats, int & UnderSize )
+{
+    firstAigDumpFile = "";
+    dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
+    fNeedMiter = !opt_mgr["--miter"];
+    fCrossStats = opt_mgr["--crossstats"] ? 1 : 0;
+    UnderSize = opt_mgr["--under"] ? stoi(opt_mgr.GetOptVal("--under")) : -1;
+
+    if(opt_mgr["--norm"])
+        Params.fNorm ^= 1;
+    if(opt_mgr["--cexmin"])
+        Params.fCexMin ^= 1;
+    if(opt_mgr["--pba_uif"])
+        Params.fPbaUif ^= 1;
+    if(opt_mgr["--pbasim"])
+        Params.fPbaSim ^= 1;
+    if(opt_mgr["--pbacex"])
+        Params.fPbaCex ^= 1;
+    if(opt_mgr["--satmin"])
+        Params.fSatMin ^= 1;
+    if(opt_mgr["--cbawb"])
+        Params.fCbaWb ^= 1;
+    if(opt_mgr["--grey"])
+        Params.fGrey ^= 1;
+    if(opt_mgr["--allwb"])
+        Params.fAllWb ^= 1;
+    if(opt_mgr["--crossonly"])
+        Params.fCrossOnly ^= 1;
+    if(opt_mgr["--grey2"])
+        Params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
+    if(opt_mgr["--sp"])
+        Params.fSuper_prove ^= 1;
+    if(opt_mgr["--simp"])
+        Params.fSimple ^= 1;
+    if(opt_mgr["--syn"])
+        Params.fSyn ^= 1;
+    if(opt_mgr["--pth"])
+        Params.fPthread ^= 1;
+    if(opt_mgr["--onewb"])
+        Params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
+    if(opt_mgr["--initallpairs"])
+        Params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
+    if(opt_mgr["--initnear"])
+        Params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
+    if(opt_mgr["--exp"])
+        Params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
+    if(opt_mgr["--par"])
+        Params.parSetting = opt_mgr.GetOptVal("--par");
+    if(opt_mgr["--solver"])
+        Params.solverSetting = opt_mgr.GetOptVal("--solver");
+    if(opt_mgr["--sim"])
+        Params.simSetting = opt_mgr.GetOptVal("--sim");
+    if(opt_mgr["--dump_states"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump_states");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
+            Params.fileStatesOut = sub_match[1].str();
+        else
+            Params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
+    }
+    if(opt_mgr["--read_states"])
+        Params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
+    if(opt_mgr["--lazysim"])
+        Params.fLazySim ^= 1;
+    if(opt_mgr["-v"])
+        Params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
+    if(opt_mgr["--timeout"])
+        Params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
+    if(opt_mgr["--seq"])
+        Params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
+    if(opt_mgr["--dump-abs"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump-abs");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
+            Params.fileAbs = sub_match[1].str();
+        else
+            Params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
+    }
+    if(opt_mgr["--dump"]) {
+        smatch sub_match;
+        string option = opt_mgr.GetOptVal("--dump");
+        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
+            Params.fileName = sub_match[1].str();
+        else
+            Params.fileName = opt_mgr.GetOptVal("--dump");
+    }
+    if ( opt_mgr["--dump-first-aig"] )
+        firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
+    set_op_types.insert(WLC_OBJ_ARI_MULTI);
+    if (opt_mgr["--adder"])
+        set_op_types.insert(WLC_OBJ_ARI_ADD);
+}
+static bool Ufar_TokenizeArgs( const char * pArgs, vector<string> & Tokens )
+{
+    string Cur;
+    char Quote = 0;
+    if ( pArgs == NULL )
+        return true;
+    for ( ; *pArgs; ++pArgs )
+    {
+        unsigned char c = (unsigned char)*pArgs;
+        if ( Quote )
+        {
+            if ( c == (unsigned char)Quote )
+                Quote = 0;
+            else if ( c == '\\' && pArgs[1] )
+                Cur += *++pArgs;
+            else
+                Cur += (char)c;
+            continue;
+        }
+        if ( c == '"' || c == '\'' )
+        {
+            Quote = (char)c;
+            continue;
+        }
+        if ( isspace(c) )
+        {
+            if ( !Cur.empty() )
+            {
+                Tokens.push_back( Cur );
+                Cur.clear();
+            }
+            continue;
+        }
+        if ( c == '\\' && pArgs[1] )
+        {
+            Cur += *++pArgs;
+            continue;
+        }
+        Cur += (char)c;
+    }
+    if ( Quote )
+        return false;
+    if ( !Cur.empty() )
+        Tokens.push_back( Cur );
+    return true;
+}
+
 
 void Ufar_Init(Abc_Frame_t *pAbc)
 {
@@ -84,39 +313,163 @@ void Ufar_Init(Abc_Frame_t *pAbc)
     //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter",          Abc_CommandCreateMiter,     0 );
 }
 
-int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId )
+int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs )
 {
     UFAR::UfarManager manager;
     timeval t1;
+    vector<string> Tokens;
+    vector<char *> Argv;
     set<unsigned> set_op_types;
-    Wlc_Ntk_t * pUse = pNtk;
+    string firstAigDumpFile, dumpLogFile;
+    string statusName;
+    int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
+    Wlc_Ntk_t * pUse = pNtk, * pNew = NULL;
     int RetValue = -1;
     if ( pNtk == NULL )
         return -1;
-    if ( Wlc_NtkPoNum(pUse) == 2 )
+    Ufar_SetDefaultParams( manager.params, nTimeOut, fVerbose, pFuncStop, RunId );
+    if ( pArgs && pArgs[0] )
     {
-        pUse = UFAR::CreateMiter( pUse, 0 );
-        if ( pUse == NULL )
+        OptMgr opt_mgr("%ufar");
+        Ufar_AddOptions( opt_mgr, manager.params );
+        if ( !Ufar_TokenizeArgs(pArgs, Tokens) )
+        {
+            cout << "Cannot parse internal %ufar option string." << endl;
             return -1;
+        }
+        Argv.reserve( Tokens.size() + 1 );
+        Argv.push_back( (char *)"%ufar" );
+        for ( size_t i = 0; i < Tokens.size(); i++ )
+            Argv.push_back( (char *)Tokens[i].c_str() );
+        if ( !opt_mgr.Parse((int)Argv.size(), Argv.data()) )
+        {
+            opt_mgr.PrintUsage();
+            return -1;
+        }
+        Ufar_ApplyOptions( opt_mgr, manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
+    }
+    else
+        set_op_types.insert( WLC_OBJ_ARI_MULTI );
+    Ufar_StopScope_t StopScope( manager.params.pFuncStop, (int)manager.params.nTimeout );
+    manager.params.pFuncStop = Ufar_StopWithTimeout;
+    if ( fNeedMiter )
+    {
+        if ( Wlc_NtkPoNum(pUse) == 2 )
+        {
+            pNew = UFAR::CreateMiter( pUse, 0 );
+            if ( pUse != pNtk )
+                Wlc_NtkFree( pUse );
+            pUse = pNew;
+            if ( pUse == NULL )
+                return -1;
+        }
+        else if ( Wlc_NtkPoNum(pUse) != 1 )
+        {
+            return -1;
+        }
     }
     else if ( Wlc_NtkPoNum(pUse) != 1 )
         return -1;
-    set_op_types.insert( WLC_OBJ_ARI_MULTI );
+    statusName = Ufar_GetStatusName( pUse );
+    if ( manager.params.fNorm )
+    {
+        pNew = UFAR::NormalizeDataTypes( pUse, set_op_types, true );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+    }
+    if ( fCrossStats )
+    {
+        Wlc_Ntk_t * pCur = pUse;
+        if ( Wlc_NtkPoNum(pCur) != 2 )
+        {
+            cout << "CrossStats requires dual outputs before mitering.\n";
+            if ( pUse != pNtk )
+                Wlc_NtkFree( pUse );
+            return -1;
+        }
+        int nObjs = Wlc_NtkObjNumMax(pCur);
+        vector<char> vConeL(nObjs, 0), vConeR(nObjs, 0);
+        auto mark_cone = [&]( int iStart, vector<char>& vMark )
+        {
+            if ( iStart < 0 || iStart >= nObjs )
+                return;
+            vector<int> stack(1, iStart);
+            while ( !stack.empty() )
+            {
+                int iObj = stack.back();
+                stack.pop_back();
+                if ( iObj < 0 || iObj >= nObjs || vMark[iObj] )
+                    continue;
+                vMark[iObj] = 1;
+                Wlc_Obj_t * pObjT = Wlc_NtkObj(pCur, iObj);
+                if ( pObjT->Type == WLC_OBJ_FO )
+                {
+                    Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(pCur, pObjT);
+                    stack.push_back( Wlc_ObjId(pCur, pFi) );
+                }
+                int iFanin, k;
+                Wlc_ObjForEachFanin( pObjT, iFanin, k )
+                    stack.push_back(iFanin);
+            }
+        };
+        int iRootL = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 0) );
+        int iRootR = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 1) );
+        mark_cone(iRootL, vConeL);
+        mark_cone(iRootR, vConeR);
+
+        int nL = 0, nR = 0, nB = 0, nN = 0;
+        Wlc_Obj_t * pObjT; int iObj;
+        Wlc_NtkForEachObj( pCur, pObjT, iObj )
+        {
+            if ( pObjT->Type != WLC_OBJ_ARI_MULTI )
+                continue;
+            bool fL = vConeL[iObj] != 0;
+            bool fR = vConeR[iObj] != 0;
+            if ( fL && fR ) nB++;
+            else if ( fL )  nL++;
+            else if ( fR )  nR++;
+            else            nN++;
+        }
+        cout << "UIF_PROVE : CrossStats: L=" << nL
+             << " R=" << nR
+             << " BOTH=" << nB
+             << " NONE=" << nN
+             << " TOTAL=" << (nL + nR + nB + nN) << endl;
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        return -1;
+    }
     if ( !UFAR::HasOperator( pUse, set_op_types ) )
     {
         if ( pUse != pNtk )
             Wlc_NtkFree( pUse );
         return -1;
     }
-    manager.params = UFAR::UfarManager::Params();
-    manager.params.RunId = RunId;
-    manager.params.pFuncStop = pFuncStop;
-    if ( nTimeOut > 0 )
-        manager.params.nTimeout = nTimeOut;
-    manager.params.iVerbosity = fVerbose ? 1 : 0;
+    if ( UnderSize >= 0 )
+    {
+        pNew = UFAR::MakeUnderApprox( pUse, UnderSize );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+        pNew = UFAR::MakeUnderApprox2( pUse, set_op_types, UnderSize );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        pUse = pNew;
+    }
+    if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
+    {
+        Gia_Man_t * pGia = UFAR::BitBlast( pUse );
+        Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
+        Gia_ManStop( pGia );
+        if ( pUse != pNtk )
+            Wlc_NtkFree( pUse );
+        return -1;
+    }
     gettimeofday( &t1, NULL );
     manager.Initialize( pUse, set_op_types );
     RetValue = manager.PerformUIFProve( t1 );
+    Ufar_DumpStatusLog( dumpLogFile, RetValue, statusName );
     if ( pUse != pNtk )
         Wlc_NtkFree( pUse );
     return RetValue;
@@ -160,141 +513,22 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     ufar_manager.params = UFAR::UfarManager::Params();
 
     OptMgr opt_mgr(argv[0]);
-    opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization");
-    opt_mgr.AddOpt("--adder", "no", "", "toggle including adders");
-    opt_mgr.AddOpt("--cexmin", ufar_manager.params.fCexMin ? "yes" : "no", "", "toggle using CEX minimization");
-    opt_mgr.AddOpt("--sim", "none", "str", "use simulation and specify its setting");
-    opt_mgr.AddOpt("-v", to_string(ufar_manager.params.iVerbosity), "num", "specify verbosity level");
-    opt_mgr.AddOpt("--seq", to_string(ufar_manager.params.nSeqLookBack), "num", "specify the number of look-back frames (0 = no sequential UIF)");
-    opt_mgr.AddOpt("--profile", "no", "", "dump time distribution");
-    opt_mgr.AddOpt("--pba_uif", ufar_manager.params.fPbaUif ? "yes" : "no", "", "toggle using proof-based refinement for UIF pairs");
-    opt_mgr.AddOpt("--lazysim", ufar_manager.params.fLazySim ? "yes" : "no", "", "toggle applying UIF pairs based on simulation");
-    opt_mgr.AddOpt("--pbasim", ufar_manager.params.fPbaSim ? "yes" : "no", "", "toggle combining pba and sim");
-    opt_mgr.AddOpt("--pbacex", ufar_manager.params.fPbaCex ? "yes" : "no", "", "toggle combining pba and cex");
-    opt_mgr.AddOpt("--satmin", ufar_manager.params.fSatMin ? "yes" : "no", "", "toggle using sat-min in pba");
-    opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing");
-    opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints");
-    opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold");
-    opt_mgr.AddOpt("--allwb", ufar_manager.params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)");
-    opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
-    opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
-    opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
-    opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
-    opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
-    opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
-    opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
-    opt_mgr.AddOpt("--solver", "none", "str", "external solver command line");
-    opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file");
-    opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file");
-    opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove");
-    opt_mgr.AddOpt("--simp", ufar_manager.params.fSimple ? "yes" : "no", "", "toggle using simple (prove)");
-    opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis");
-    opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads");
-    opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing");
-    opt_mgr.AddOpt("--initallpairs", to_string(ufar_manager.params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)");
-    opt_mgr.AddOpt("--initnear", to_string(ufar_manager.params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output");
-    opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)");
-    opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode");
-    opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem");
-    opt_mgr.AddOpt("--under", "-1", "num", "try under-approximation with the given size");
+    set<unsigned> set_op_types;
+    string firstAigDumpFile = "";
+    string dumpLogFile = "";
+    int fNeedMiter = 1, fCrossStats = 0, UnderSize = -1;
+    Ufar_AddOptions( opt_mgr, ufar_manager.params );
     if(!opt_mgr.Parse(argc, argv)) {
         opt_mgr.PrintUsage();
         cout << "\n       This command was developed by Yen-Sheng Ho at UC Berkeley in 2015.\n";
         cout << "       https://people.eecs.berkeley.edu/~alanmi/publications/2016/fmcad16_uif.pdf \n"; 
         return 0;
     }
-
-    if(opt_mgr["--norm"])
-        ufar_manager.params.fNorm ^= 1;
-    if(opt_mgr["--cexmin"])
-        ufar_manager.params.fCexMin ^= 1;
-    if(opt_mgr["--pba_uif"])
-        ufar_manager.params.fPbaUif ^= 1;
-    if(opt_mgr["--pbasim"])
-        ufar_manager.params.fPbaSim ^= 1;
-    if(opt_mgr["--pbacex"])
-        ufar_manager.params.fPbaCex ^= 1;
-    if(opt_mgr["--satmin"])
-        ufar_manager.params.fSatMin ^= 1;
-    if(opt_mgr["--cbawb"])
-        ufar_manager.params.fCbaWb ^= 1;
-    if(opt_mgr["--grey"])
-        ufar_manager.params.fGrey ^= 1;
-    if(opt_mgr["--allwb"])
-        ufar_manager.params.fAllWb ^= 1;
-    if(opt_mgr["--crossonly"])
-        ufar_manager.params.fCrossOnly ^= 1;
-    if(opt_mgr["--grey2"])
-        ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2"));
-    if(opt_mgr["--sp"])
-        ufar_manager.params.fSuper_prove ^= 1;
-    if(opt_mgr["--simp"])
-        ufar_manager.params.fSimple ^= 1;
-    if(opt_mgr["--syn"])
-        ufar_manager.params.fSyn ^= 1;
-    if(opt_mgr["--pth"])
-        ufar_manager.params.fPthread ^= 1;
-    if(opt_mgr["--onewb"])
-        ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb"));
-    if(opt_mgr["--initallpairs"])
-        ufar_manager.params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs"));
-    if(opt_mgr["--initnear"])
-        ufar_manager.params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear"));
-    if(opt_mgr["--exp"])
-        ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp"));
-    if(opt_mgr["--par"])
-        ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par");
-    if(opt_mgr["--solver"])
-        ufar_manager.params.solverSetting = opt_mgr.GetOptVal("--solver");
-    if(opt_mgr["--sim"])
-        ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim");
-    if(opt_mgr["--dump_states"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump_states");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
-            ufar_manager.params.fileStatesOut = sub_match[1].str();
-        else
-            ufar_manager.params.fileStatesOut = opt_mgr.GetOptVal("--dump_states");
-    }
-    if(opt_mgr["--read_states"])
-        ufar_manager.params.fileStatesIn = opt_mgr.GetOptVal("--read_states");
-    if(opt_mgr["--lazysim"])
-        ufar_manager.params.fLazySim ^= 1;
-    if(opt_mgr["-v"])
-        ufar_manager.params.iVerbosity = stoi(opt_mgr.GetOptVal("-v"));
-    if(opt_mgr["--timeout"])
-        ufar_manager.params.nTimeout = stoi(opt_mgr.GetOptVal("--timeout"));
-    if(opt_mgr["--seq"])
-        ufar_manager.params.nSeqLookBack = stoi(opt_mgr.GetOptVal("--seq"));
-    if(opt_mgr["--dump-abs"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump-abs");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)")))
-            ufar_manager.params.fileAbs = sub_match[1].str();
-        else
-            ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
-    }
-    if(opt_mgr["--dump"]) {
-        smatch sub_match;
-        string option = opt_mgr.GetOptVal("--dump");
-        if(regex_search(option, sub_match, regex(R"(/?(\w+\.v)$)")))
-            ufar_manager.params.fileName = sub_match[1].str();
-        else
-            ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump");
-    }
-    string firstAigDumpFile = "";
-    if ( opt_mgr["--dump-first-aig"] )
-        firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig");
+    Ufar_ApplyOptions( opt_mgr, ufar_manager.params, set_op_types, firstAigDumpFile, dumpLogFile, fNeedMiter, fCrossStats, UnderSize );
 
     // ufar_manager.DumpParams();
     LogT::prefix = "UIF_PROVE";
-    string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
     string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) );
-
-    set<unsigned> set_op_types;
-    set_op_types.insert(WLC_OBJ_ARI_MULTI);
-    if (opt_mgr["--adder"])
-        set_op_types.insert(WLC_OBJ_ARI_ADD);
     if (!UFAR::HasOperator(Wlc_AbcGetNtk(pAbc), set_op_types)) {
         cout << "There is no operator for UIF.\n";
         return 0;
@@ -304,7 +538,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     timeval t1, t2;
     gettimeofday(&t1, NULL);
 
-    if (!opt_mgr["--miter"]) {
+    if (fNeedMiter) {
         if (Wlc_NtkPoNum(Wlc_AbcGetNtk(pAbc)) != 2) {
             cout << "The current design doesn't have dual outputs.\n";
             return 0;
@@ -318,7 +552,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         Wlc_AbcUpdateNtk(pAbc, pNew);
     }
 
-    if ( opt_mgr["--crossstats"] )
+    if ( fCrossStats )
     {
         Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
         if ( Wlc_NtkPoNum(pCur) != 2 )
@@ -380,10 +614,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         return 0;
     }
 
-    if (opt_mgr["--under"]) {
-        pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
+    if ( UnderSize >= 0 ) {
+        pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), UnderSize);
         Wlc_AbcUpdateNtk(pAbc, pNew);
-        pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, stoi(opt_mgr.GetOptVal("--under")));
+        pNew = UFAR::MakeUnderApprox2(Wlc_AbcGetNtk(pAbc), set_op_types, UnderSize);
         Wlc_AbcUpdateNtk(pAbc, pNew);
         Wlc_WriteVer(Wlc_AbcGetNtk(pAbc), "UND.v", 0, 0);
     }
diff --git a/src/opt/ufar/UfarCmd.h b/src/opt/ufar/UfarCmd.h
index 52dfc8bb8..b44863ca3 100755
--- a/src/opt/ufar/UfarCmd.h
+++ b/src/opt/ufar/UfarCmd.h
@@ -15,7 +15,7 @@ ABC_NAMESPACE_HEADER_START
 void Ufar_Init(Abc_Frame_t *pAbc);
 
 typedef struct Wlc_Ntk_t_ Wlc_Ntk_t;
-extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
+extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp
index b0cb5bd15..2e6782731 100755
--- a/src/opt/untk/NtkNtk.cpp
+++ b/src/opt/untk/NtkNtk.cpp
@@ -805,7 +805,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
     Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple(pNtk);
     Wlc_NtkCleanCopy( p );
     int nOrigObjNum = Wlc_NtkObjNumMax(p);
-    Wlc_NtkTransferNames( p, pNtk );
+    if ( !Wlc_NtkHasNameId(p) && Wlc_NtkHasNameId(pNtk) )
+        Wlc_NtkTransferNames( p, pNtk );
 
     Wlc_Obj_t * pObj;
     int i, iObjConst0;
@@ -872,7 +873,8 @@ Wlc_Ntk_t * AddConstFlops( Wlc_Ntk_t * pNtk, const set<unsigned>& types )
     ModifyMarkedNodes(p, nOrigObjNum, create_ff_and_mux);
 
     Wlc_Ntk_t * pNew = Wlc_NtkDupDfsSimple( p );
-    Wlc_NtkTransferNames( pNew, p );
+    if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNew, p );
 
     Wlc_NtkFree( p );
 
@@ -1058,7 +1060,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
     Wlc_Ntk_t *pNtk, *pNew;
 
     pNtk = Wlc_NtkDupDfsSimple(p);
-    Wlc_NtkTransferNames( pNtk, p );
+    if ( !Wlc_NtkHasNameId(pNtk) && Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNtk, p );
 
     Wlc_Obj_t *pObj;
     int i, iFanin0, iFanin1;
@@ -1117,7 +1120,8 @@ Wlc_Ntk_t * NormalizeDataTypes(Wlc_Ntk_t * p, const set<unsigned>& types, bool f
     Vec_IntFree(vFanins);
 
     pNew = Wlc_NtkDupDfsSimple(pNtk);
-    Wlc_NtkTransferNames( pNew, pNtk );
+    if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(pNtk) )
+        Wlc_NtkTransferNames( pNew, pNtk );
     Wlc_NtkFree(pNtk);
 
     return pNew;
@@ -1266,11 +1270,15 @@ static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string&
     Io_Write( pAbcNtk, (char *)pAigFile, IO_FILE_AIGER );
     std::remove( "status.txt" );
     std::remove( "log.txt" );
-    string command = solverCmd;
-    if ( command.find(pAigFile) == string::npos )
-        command += string(" ") + pAigFile;
+    string solverCall = solverCmd;
+    string command;
+    if ( solverCall.find(pAigFile) == string::npos )
+        solverCall += string(" ") + pAigFile;
     if ( nRuntimeLimitSec > 0 )
-        command += " " + to_string(nRuntimeLimitSec);
+        solverCall += " " + to_string(nRuntimeLimitSec);
+    command = solverCall;
+    if ( nRuntimeLimitSec > 0 )
+        command = "timeout " + to_string(nRuntimeLimitSec) + " " + command;
     command += " > log.txt 2>&1";
     LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
     int res = system( command.c_str() );
diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c
index 8b7aa2868..43395aa23 100644
--- a/src/proof/cec/cecProve.c
+++ b/src/proof/cec/cecProve.c
@@ -61,15 +61,15 @@ struct Cec_SproveTrace_t_;
 static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
 static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
 static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
-static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
+static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
 static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
 static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
 
-extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId );
+extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
 
 #ifndef ABC_USE_PTHREADS
 
-int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile ) { return -1; }
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs ) { return -1; }
 int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, int * pnTimeOut2, int * pnTimeOut3, int * pfUseUif ) { return 0; }
 int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
 
@@ -104,6 +104,7 @@ typedef struct Par_ThData_t_
     int         fVerbose;
     int         nTimeOutU;
     Wlc_Ntk_t * pWlc;
+    const char * pUfarArgs;
     int         WorkerId;
     int         StageId;
     int         NetId;
@@ -152,6 +153,7 @@ struct Cec_SprovePlan_t_
     int nTimeOut2;
     int nTimeOut3;
     int fUseUif;
+    char * pUfarArgs;
     int nStages;
     Cec_SproveStage_t Stages[SPROVE_STAGE_MAX];
 };
@@ -309,6 +311,13 @@ static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines,
 {
     int i, nEngines = nProcs + (fUseUif ? 1 : 0);
     assert( nEngines >= 1 && nEngines <= PAR_THR_MAX );
+    if ( fUseUif && nProcs == 6 )
+    {
+        int UifEngines[7] = { 0, 1, 2, 3, 4, PAR_ENGINE_GLA, PAR_ENGINE_UFAR };
+        memcpy( pEngines, UifEngines, sizeof(UifEngines) );
+        *pnEngines = 7;
+        return;
+    }
     for ( i = 0; i < nEngines; i++ )
     {
         if ( fUseUif && i == nEngines - 1 )
@@ -320,7 +329,25 @@ static void Cec_SproveDeriveEngineList( int nProcs, int fUseUif, int * pEngines,
     }
     *pnEngines = nEngines;
 }
-static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif )
+static void Cec_SproveTrimLineEnd( char * pLine )
+{
+    int nSize = strlen( pLine );
+    while ( nSize > 0 && (pLine[nSize - 1] == '\n' || pLine[nSize - 1] == '\r') )
+        pLine[--nSize] = 0;
+}
+static void Cec_SprovePlanSetUfarArgs( Cec_SprovePlan_t * pPlan, const char * pUfarArgs )
+{
+    ABC_FREE( pPlan->pUfarArgs );
+    pPlan->pUfarArgs = NULL;
+    if ( pUfarArgs && pUfarArgs[0] )
+        pPlan->pUfarArgs = Abc_UtilStrsav( (char *)pUfarArgs );
+}
+static void Cec_SprovePlanFree( Cec_SprovePlan_t * pPlan )
+{
+    ABC_FREE( pPlan->pUfarArgs );
+    pPlan->pUfarArgs = NULL;
+}
+static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, const char * pUfarArgs )
 {
     int nEngines;
     memset( pPlan, 0, sizeof(Cec_SprovePlan_t) );
@@ -334,6 +361,7 @@ static void Cec_SprovePlanDefault( Cec_SprovePlan_t * pPlan, int nProcs, int nTi
     pPlan->nTimeOut2 = nTimeOut2;
     pPlan->nTimeOut3 = nTimeOut3;
     pPlan->fUseUif = fUseUif;
+    Cec_SprovePlanSetUfarArgs( pPlan, pUfarArgs );
     pPlan->nStages = 4;
     Cec_SproveDeriveEngineList( nProcs, fUseUif, pPlan->Stages[0].RoundEngines, &nEngines );
 
@@ -408,6 +436,8 @@ static void Cec_SproveTraceOpen( Cec_SproveTrace_t * pTrace, Gia_Man_t * p, Cec_
     Cec_SproveTraceWrite( pTrace, "SPROVE_REPLAY 1" );
     Cec_SproveTraceWrite( pTrace, "CASE %s", pProbName ? pProbName : "(none)" );
     Cec_SproveTraceWrite( pTrace, "PARAMS P=%d T=%d U=%d W=%d UIF=%d", pPlan->nProcs, pPlan->nTimeOut, pPlan->nTimeOut2, pPlan->nTimeOut3, pPlan->fUseUif );
+    if ( pPlan->pUfarArgs && pPlan->pUfarArgs[0] )
+        Cec_SproveTraceWrite( pTrace, "UFAR_ARGS %s", pPlan->pUfarArgs );
     Cec_SproveTraceWrite( pTrace, "" );
     Cec_SproveTraceWrite( pTrace, "PLAN_BEGIN" );
     for ( i = 0; i < pPlan->nStages; i++ )
@@ -479,12 +509,20 @@ static int Cec_SproveReplayReadParamsInt( char * pFileName, Cec_SprovePlan_t * p
             pPlan->nTimeOut3 = atoi(Value);
             if ( !Cec_SproveFindValue(Buffer, "UIF=", Value, sizeof(Value)) ) break;
             pPlan->fUseUif = atoi(Value);
+        }
+        else if ( strncmp(Buffer, "UFAR_ARGS ", 10) == 0 )
+        {
+            Cec_SproveTrimLineEnd( Buffer );
+            Cec_SprovePlanSetUfarArgs( pPlan, Buffer + 10 );
+        }
+        else if ( pPlan->nProcs > 0 && (strncmp(Buffer, "PLAN_BEGIN", 10) == 0 || strncmp(Buffer, "OBSERVED_BEGIN", 14) == 0) )
+        {
             fclose( pFile );
             return 1;
         }
     }
     fclose( pFile );
-    return 0;
+    return pPlan->nProcs > 0;
 }
 static int Cec_SproveReplayReadPlan( char * pFileName, Cec_SprovePlan_t * pPlan )
 {
@@ -717,7 +755,7 @@ static int Cec_SproveExecutePlan( Gia_Man_t * p, Cec_SprovePlan_t * pPlan, Wlc_N
             }
             Cec_SproveTraceWrite( &Trace, "START kind=round stage=%d net=%s timeout=%d t=%llu",
                 pStage->Id, Cec_SproveNetName(pStage->RoundNet), pStage->RoundTimeout, Cec_SproveClockToMs( Cec_SproveTraceTime(&Trace) ) );
-            Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pPlan->nTimeOut3, pWlc, fVerbose,
+            Cec_GiaInitThreads( ThData, pStage->nRoundEngines, pRoundNet, pStage->RoundTimeout, pStage->RoundTimeout, pWlc, pPlan->pUfarArgs, fVerbose,
                 fThreadsStarted ? NULL : WorkerThread, &Share, pStage->RoundEngines, pStage->Id, pStage->RoundNet, &Trace );
             fThreadsStarted = 1;
         }
@@ -918,7 +956,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
         if ( pThData && pThData->pWlc )
         {
             g_pUfarShare = pThData->pShare;
-            RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0 );
+            RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0, pThData->pUfarArgs );
             g_pUfarShare = NULL;
         }
     }
@@ -1070,7 +1108,7 @@ static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers )
         assert( status == 0 );
     }
 }
-static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
+static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, Cec_SproveTrace_t * pTrace )
 {
     int i, status;
     assert( nWorkers <= PAR_THR_MAX );
@@ -1088,6 +1126,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
             ThData[i].fVerbose = fVerbose;
             ThData[i].nTimeOutU= nTimeOutU;
             ThData[i].pWlc     = pWlc;
+            ThData[i].pUfarArgs= pUfarArgs;
             ThData[i].WorkerId = i;
             ThData[i].StageId  = StageId;
             ThData[i].NetId    = NetId;
@@ -1115,6 +1154,7 @@ static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t *
         ThData[i].fVerbose = fVerbose;
         ThData[i].nTimeOutU= nTimeOutU;
         ThData[i].pWlc     = pWlc;
+        ThData[i].pUfarArgs= pUfarArgs;
         ThData[i].WorkerId = i;
         ThData[i].StageId  = StageId;
         ThData[i].NetId    = NetId;
@@ -1188,22 +1228,29 @@ int Cec_GiaReplayReadParams( char * pFileName, int * pnProcs, int * pnTimeOut, i
         *pnTimeOut3 = Plan.nTimeOut3;
     if ( pfUseUif )
         *pfUseUif = Plan.fUseUif;
+    Cec_SprovePlanFree( &Plan );
     return 1;
 }
-int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile )
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent, char * pReplayFile, char * pUfarArgs )
 {
     Cec_SprovePlan_t Plan;
-    Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif );
+    int RetValue;
+    Cec_SprovePlanDefault( &Plan, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pUfarArgs );
     assert( nProcs >= 1 && nProcs <= 6 );
     assert( nProcs + (fUseUif ? 1 : 0) <= PAR_THR_MAX );
-    return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, pReplayFile );
+    Cec_SprovePlanFree( &Plan );
+    return RetValue;
 }
 int Cec_GiaReplayTest( Gia_Man_t * p, Wlc_Ntk_t * pWlc, char * pFileName, int fVerbose, int fVeryVerbose, int fSilent )
 {
     Cec_SprovePlan_t Plan;
+    int RetValue;
     if ( !Cec_SproveReplayReadPlan( pFileName, &Plan ) )
         return -1;
-    return Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
+    RetValue = Cec_SproveExecutePlan( p, &Plan, pWlc, fVerbose, fVeryVerbose, fSilent, NULL );
+    Cec_SprovePlanFree( &Plan );
+    return RetValue;
 }
 
 #endif // pthreads are used