From c1ed182d38d2c9dd22f5d531337167ec38c18a15 Mon Sep 17 00:00:00 2001
From: phyzhenli <48823046+phyzhenli@users.noreply.github.com>
Date: Tue, 6 Jan 2026 10:34:26 +0800
Subject: [PATCH 1/6] Fix &synch2 crash with creating wrong mapping

---
 src/aig/gia/giaLf.c | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c
index 130660050..3732794ee 100644
--- a/src/aig/gia/giaLf.c
+++ b/src/aig/gia/giaLf.c
@@ -1838,6 +1838,12 @@ static inline int Lf_ManDerivePart( Lf_Man_t * p, Gia_Man_t * pNew, Vec_Int_t *
     }
     pTruth = Lf_CutTruth( p, pCut );
     iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
+    // do not create LUT in the simple case
+    if ( Abc_Lit2Var(iLit) == 0 )
+        return iLit;
+    Vec_IntForEachEntry( vLeaves, iTemp, k )
+        if ( Abc_Lit2Var(iLit) == Abc_Lit2Var(iTemp) )
+            return iLit;
     // create mapping
     Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) );
     Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );

From ee40e40d09685734f15466410c44bb1e1b0a812e Mon Sep 17 00:00:00 2001
From: Drew Lewis <cannada@google.com>
Date: Mon, 2 Mar 2026 22:22:27 +0000
Subject: [PATCH 2/6] Have the buffer grow with a 2x factor to avoid O(n^2)
 work when reading big files.

Signed-off-by: Drew Lewis <cannada@google.com>
---
 src/map/scl/sclLiberty.c | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c
index 2064fde69..06d40c84b 100644
--- a/src/map/scl/sclLiberty.c
+++ b/src/map/scl/sclLiberty.c
@@ -559,14 +559,17 @@ static char * Io_LibLoadFileGz( char * pFileName, long * pnFileSize )
     const int READ_BLOCK_SIZE = 100000;
     gzFile pFile;
     char * pContents;
-    long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
+    long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE, nCapacity = READ_BLOCK_SIZE;
     pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
-    pContents = ABC_ALLOC( char, nFileSize );
+    pContents = ABC_ALLOC( char, nCapacity );
     readBlock = 0;
     while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
         //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);
         nFileSize += READ_BLOCK_SIZE;
-        pContents = ABC_REALLOC(char, pContents, nFileSize);
+        if ( nFileSize > nCapacity ) {
+            nCapacity *= 2;
+            pContents = ABC_REALLOC(char, pContents, nCapacity);
+        }
         ++readBlock;
     }
     //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead);

From c92cfab80bf75372f7597f0e4554d111ba735cbd Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 8 Mar 2026 10:25:15 -0700
Subject: [PATCH 3/6] Adding new line at the end of AIGER files.

---
 src/aig/gia/giaAiger.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 39fed2fd4..c37c3ea9e 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1297,7 +1297,7 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p )
         Gia_AigerWriteUnsigned( vBuffer, uLit  - uLit1 );
         Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 );
     }
-    Vec_StrPrintStr( vBuffer, "c" );
+    Vec_StrPrintStr( vBuffer, "c\n" );
     return vBuffer;
 }
 

From ba69519d736763531d141859caffcca887b664f7 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 8 Mar 2026 10:26:27 -0700
Subject: [PATCH 4/6] Adding command for calling external solvers.

---
 src/base/cmd/cmd.c | 75 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 0bb4b412b..bbe3b7d8e 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -67,6 +67,7 @@ static int CmdCommandCapo          ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int CmdCommandStarter       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandAutoTuner     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandSolver        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandSolver2       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -123,6 +124,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various", "starter",     CmdCommandStarter,         0 );
     Cmd_CommandAdd( pAbc, "Various", "autotuner",   CmdCommandAutoTuner,       0 );
     Cmd_CommandAdd( pAbc, "Various", "&solver",     CmdCommandSolver,          0 );
+    Cmd_CommandAdd( pAbc, "Various", "&solver2",    CmdCommandSolver2,         0 );
 
     Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn,  0 );
 }
@@ -2971,6 +2973,79 @@ usage:
     return 1;
 }
 
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int CmdCommandSolver2( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    char Command[2000];
+    int i;
+
+    if ( argc > 1 )
+    {
+        if ( strcmp( argv[1], "-h" ) == 0 )
+            goto usage;
+        if ( strcmp( argv[1], "-?" ) == 0 )
+            goto usage;
+    }
+
+#if defined(__wasm)
+    fprintf( pAbc->Err, "Unsupported command.\n" );
+    return 1;
+#else
+    // Check if solver binary exists in current directory or PATH
+    if ( (pFile = fopen( "./solver", "r" )) != NULL )
+    {
+        sprintf( Command, "%s", "./solver" );
+        fclose( pFile );
+    }
+    else
+    {
+        char CheckCommand[100];
+        sprintf( CheckCommand, "which solver > /dev/null 2>&1" );
+        if ( system( CheckCommand ) != 0 )
+        {
+            fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" );
+            goto usage;
+        }
+        sprintf( Command, "%s", "solver" );
+    }
+
+    // Append user-provided arguments as-is: solver <args>
+    for ( i = 1; i < argc; i++ )
+    {
+        strcat( Command, " " );
+        strcat( Command, argv[i] );
+    }
+
+    fprintf( pAbc->Out, "Executing command: %s\n", Command );
+    if ( system( Command ) == -1 )
+    {
+        fprintf( pAbc->Err, "The following command has failed:\n" );
+        fprintf( pAbc->Err, "\"%s\"\n", Command );
+        return 1;
+    }
+#endif
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "\tusage: &solver2 <args>\n");
+    fprintf( pAbc->Err, "\t           run the external solver as \"solver <args>\"\n" );
+    fprintf( pAbc->Err, "\t-h      :  print the command usage\n" );
+    fprintf( pAbc->Err, "\t<args>  :  all arguments passed directly to solver\n" );
+    return 1;
+}
+
 /**Function********************************************************************
 
   Synopsis    [Print the version string.]

From a745d5ec817bf1fce32d205a0bb586e10a052516 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 8 Mar 2026 10:27:12 -0700
Subject: [PATCH 5/6] Adding profiling to %ufar.

---
 src/opt/ufar/UfarCmd.cpp | 144 ++++++++++++++++-
 src/opt/ufar/UfarMgr.cpp | 329 ++++++++++++++++++++++++++++++++++++++-
 src/opt/ufar/UfarMgr.h   |  31 +++-
 src/opt/untk/NtkNtk.cpp  |  99 +++++++++++-
 src/opt/untk/NtkNtk.h    |   4 +-
 src/opt/util/util.cpp    |  27 +++-
 6 files changed, 619 insertions(+), 15 deletions(-)

diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp
index 37728b04d..6ac2320ff 100755
--- a/src/opt/ufar/UfarCmd.cpp
+++ b/src/opt/ufar/UfarCmd.cpp
@@ -15,8 +15,11 @@
 #include <iomanip>
 #include <climits>
 #include <regex>
+#include <cstdlib>
+#include <cstdio>
 
 #include "base/wlc/wlc.h"
+#include "aig/gia/giaAig.h"
 #include "opt/ufar/UfarCmd.h"
 #include "opt/ufar/UfarMgr.h"
 #include "opt/untk/NtkNtk.h"
@@ -120,6 +123,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         cout << "There is no current design.\n";
         return 0;
     }
+    // Make each %ufar invocation stateless: always start from factory defaults.
+    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");
@@ -137,9 +142,14 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     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-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");
@@ -147,6 +157,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     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");
@@ -174,6 +186,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         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"])
@@ -186,10 +202,16 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         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"]) {
@@ -216,7 +238,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         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");
+            ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs");
     }
     if(opt_mgr["--dump"]) {
         smatch sub_match;
@@ -226,6 +248,9 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         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_manager.DumpParams();
     LogT::prefix = "UIF_PROVE";
@@ -257,6 +282,68 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
         Wlc_AbcUpdateNtk(pAbc, pNew);
     }
 
+    if ( opt_mgr["--crossstats"] )
+    {
+        Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc);
+        if ( Wlc_NtkPoNum(pCur) != 2 )
+        {
+            cout << "CrossStats requires dual outputs before mitering.\n";
+            return 0;
+        }
+        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);
+                // Sequential traversal: from flop output (FO) continue to corresponding flop input (FI).
+                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;
+        //fflush(stdout);
+        //exit(1);
+        return 0;
+    }
+
     if (opt_mgr["--under"]) {
         pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under")));
         Wlc_AbcUpdateNtk(pAbc, pNew);
@@ -267,6 +354,12 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
 
     Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc));
     Gia_ManPrintStats( pGia, NULL );
+    if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" )
+    {
+        Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() );
+        Gia_ManStop( pGia );
+        return 0;
+    }
     Gia_ManStop( pGia );
 
     ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types);
@@ -283,14 +376,61 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
     gettimeofday(&t2, NULL);
     unsigned tTotal = elapsed_time_usec(t1, t2);
     if(opt_mgr["--profile"]) {
+        unsigned nCexChecks = 0, nBitBlasts = 0;
+        unsigned long long tBitBlastUsec = 0, tCexCheckUsec = 0;
+        UFAR::Ufar_GetOrigCexStats(&nCexChecks, &nBitBlasts, &tBitBlastUsec, &tCexCheckUsec);
+        LOG(0) << "OrigCexStats: checks = " << nCexChecks
+               << ", bitblasts = " << nBitBlasts
+               << ", blast_time = " << fixed << setprecision(4) << ((double)tBitBlastUsec / 1000000.0)
+               << " sec [" << (tTotal ? (100.0 * (double)tBitBlastUsec / (double)tTotal) : 0.0) << "%]"
+               << ", cex_check_time = " << ((double)tCexCheckUsec / 1000000.0)
+               << " sec [" << (tTotal ? (100.0 * (double)tCexCheckUsec / (double)tTotal) : 0.0) << "%]";
         auto log_profile = [&](const string& str, abctime t) {
-          LOG(1) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
+          LOG(0) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]";
+        };
+        auto pct = [&](unsigned n, unsigned d) {
+            return d ? 100.0 * (double)n / (double)d : 0.0;
         };
         log_profile("BLSolver  ", ufar_manager.profile.tBLSolver);
         log_profile("UifRefine ", ufar_manager.profile.tUifRefine);
         log_profile("WbRefine  ", ufar_manager.profile.tWbRefine);
         log_profile("UifSim    ", ufar_manager.profile.tUifSim);
         log_profile("GbRefine  ", ufar_manager.profile.tGbRefine);
+        log_profile("CexCheck  ", ufar_manager.profile.tCexCheckOrig);
+        {
+            unsigned long long tKnown = (unsigned long long)ufar_manager.profile.tBLSolver
+                                      + (unsigned long long)ufar_manager.profile.tUifRefine
+                                      + (unsigned long long)ufar_manager.profile.tWbRefine
+                                      + (unsigned long long)ufar_manager.profile.tUifSim
+                                      + (unsigned long long)ufar_manager.profile.tGbRefine
+                                      + (unsigned long long)ufar_manager.profile.tCexCheckOrig;
+            unsigned long long tUnaccounted = (tTotal > tKnown) ? (tTotal - tKnown) : 0;
+            LOG(0) << "Unaccounted time = " << fixed << setprecision(4) << setw(8)
+                   << ((double)tUnaccounted / 1000000.0) << " sec [" << setw(7)
+                   << (tTotal ? (double)tUnaccounted * 100.0 / (double)tTotal : 0.0) << "%]";
+        }
+        LOG(0) << "UFAR calls: verify = " << ufar_manager.profile.nVerifyCalls
+               << " (sat = " << ufar_manager.profile.nSatCalls
+               << ", unsat = " << ufar_manager.profile.nUnsatCalls
+               << ", undec = " << ufar_manager.profile.nUnknownCalls << ")";
+        LOG(0) << "UFAR cex  : real = " << ufar_manager.profile.nRealCex
+               << ", spurious = " << ufar_manager.profile.nSpuriousCex
+               << " [" << fixed << setprecision(1)
+               << pct(ufar_manager.profile.nSpuriousCex, ufar_manager.profile.nSatCalls)
+               << "% spurious among SAT-abstraction]";
+        LOG(0) << "UFAR ref  : iters_uif = " << ufar_manager.profile.nIterUif
+               << ", iters_wb = " << ufar_manager.profile.nIterWb
+               << ", pairs_added = " << ufar_manager.profile.nUifPairsAdded
+               << ", mul_mul_pairs_added = " << ufar_manager.profile.nUifMulMulPairsAdded
+               << ", wb_added = " << ufar_manager.profile.nWbAdded;
+        LOG(0) << "UFAR size : max_pairs = " << ufar_manager.profile.nMaxUifPairs
+               << ", max_white_boxes = " << ufar_manager.profile.nMaxWhiteBoxes;
+        if ( ufar_manager.profile.nVerifyCalls ) {
+            LOG(0) << "UFAR avg  : blsolve_call = "
+                   << fixed << setprecision(4)
+                   << (double)ufar_manager.profile.tBLSolver / 1000000.0 / (double)ufar_manager.profile.nVerifyCalls
+                   << " sec/call";
+        }
     }
 
     LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec";
diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp
index 45487af77..b2177c275 100755
--- a/src/opt/ufar/UfarMgr.cpp
+++ b/src/opt/ufar/UfarMgr.cpp
@@ -13,6 +13,7 @@
 #include <algorithm>
 #include <array>
 #include <regex>
+#include <queue>
 
 #ifdef _WIN32
 #include <windows.h>
@@ -35,6 +36,27 @@ static inline unsigned log_level() {
     return LogT::loglevel;
 }
 
+static unsigned           s_nOrigCexChecks    = 0;
+static unsigned           s_nOrigBitBlasts    = 0;
+static unsigned long long s_tOrigBitBlastUsec = 0;
+static unsigned long long s_tOrigCexCheckUsec = 0;
+
+void Ufar_ResetOrigCexStats()
+{
+    s_nOrigCexChecks    = 0;
+    s_nOrigBitBlasts    = 0;
+    s_tOrigBitBlastUsec = 0;
+    s_tOrigCexCheckUsec = 0;
+}
+
+void Ufar_GetOrigCexStats( unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec )
+{
+    if ( pChecks )       *pChecks       = s_nOrigCexChecks;
+    if ( pBitBlasts )    *pBitBlasts    = s_nOrigBitBlasts;
+    if ( pBitBlastUsec ) *pBitBlastUsec = s_tOrigBitBlastUsec;
+    if ( pCexCheckUsec ) *pCexCheckUsec = s_tOrigCexCheckUsec;
+}
+
 static void split(const string &s, char delim, vector<string>& elems) {
     stringstream ss(s);
     string item;
@@ -132,7 +154,14 @@ static bool verify_cex_direct(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex) {
 }
 
 static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
+    timeval t1, t2, tCheck1, tCheck2;
+    gettimeofday(&tCheck1, NULL);
+    gettimeofday(&t1, NULL);
     Gia_Man_t * pGiaOrig = BitBlast(pOrig);
+    gettimeofday(&t2, NULL);
+    s_nOrigCexChecks++;
+    s_nOrigBitBlasts++;
+    s_tOrigBitBlastUsec += elapsed_time_usec(t1, t2);
 
     unsigned nbits_orig_pis = compute_bit_level_pi_num(pOrig);
     int nbits_ppis = pCex->nPis - Gia_ManPiNum(pGiaOrig);
@@ -161,6 +190,9 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
         Gia_ManForEachPo( pGiaOrig, pObj, i ) {
             if (pObj->Value==1) {
                 LOG(3) << "CEX is real.";
+                Gia_ManStop(pGiaOrig);
+                gettimeofday(&tCheck2, NULL);
+                s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
                 return true;
             }
         }
@@ -168,6 +200,8 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) {
 
     Gia_ManStop(pGiaOrig);
     LOG(3) << "CEX is spurious.";
+    gettimeofday(&tCheck2, NULL);
+    s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2);
     return false;
 }
 
@@ -949,6 +983,8 @@ UfarManager::Params::Params() :
                 fGrey(false),
                 nGrey(0),
                 fNorm(true),
+                fAllWb(false),
+                fCrossOnly(false),
                 fSuper_prove(false),
                 fSimple(false),
                 fSyn(false),
@@ -956,21 +992,26 @@ UfarManager::Params::Params() :
                 iOneWb(-1),
                 iExp(-1),
                 nConstraintLimit(65536),
+                nInitAllPairsLimit(0),
+                nInitNearMults(0),
                 iVerbosity(0),
                 nSeqLookBack(0),
                 nTimeout(65536)
             {}
-UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL) {}
+UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL), _fCrossReady(false) {}
 
 UfarManager::~UfarManager() {
     if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
 }
 
 void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
+    Ufar_ResetOrigCexStats();
+    LogT::loglevel = params.iVerbosity;
     if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk);
     _vec_orig_names.clear();
     _vec_op_ids.clear();
     _vec_op_blackbox_marks.clear();
+    _vec_op_side.clear();
     _vec_op_greyness.clear();
     _set_uif_pairs.clear();
     _set_uif_sim_pairs.clear();
@@ -1001,12 +1042,211 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
     }
 
     _vec_op_blackbox_marks.resize(_vec_op_ids.size(), true);
+    _vec_op_side.resize(_vec_op_ids.size(), 0);
+    _fCrossReady = false;
+    if ( params.fAllWb )
+        std::fill( _vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false );
+
+    if ( params.fCrossOnly )
+    {
+        int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
+        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(_pOrigNtk, iObj);
+                // Sequential traversal: from flop output (FO) continue to corresponding flop input (FI).
+                if ( pObjT->Type == WLC_OBJ_FO )
+                {
+                    Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT);
+                    stack.push_back( Wlc_ObjId(_pOrigNtk, pFi) );
+                }
+                int iFanin, k;
+                Wlc_ObjForEachFanin( pObjT, iFanin, k )
+                    stack.push_back(iFanin);
+            }
+        };
+
+        if ( Wlc_NtkPoNum(_pOrigNtk) == 1 )
+        {
+            Wlc_Obj_t * pPo = Wlc_NtkPo(_pOrigNtk, 0);
+            int iMiter = Wlc_ObjFaninId0(pPo);
+            if ( iMiter >= 0 && iMiter < nObjs )
+            {
+                Wlc_Obj_t * pMit = Wlc_NtkObj(_pOrigNtk, iMiter);
+                if ( Wlc_ObjFaninNum(pMit) >= 2 )
+                {
+                    int iL = Wlc_ObjFaninId0(pMit);
+                    int iR = Wlc_ObjFaninId1(pMit);
+                    mark_cone(iL, vConeL);
+                    mark_cone(iR, vConeR);
+                    _fCrossReady = true;
+                }
+            }
+        }
+        if ( _fCrossReady )
+        {
+            int nL = 0, nR = 0, nB = 0, nN = 0;
+            for ( size_t iOp = 0; iOp < _vec_op_ids.size(); ++iOp )
+            {
+                int iObj = _vec_op_ids[iOp];
+                bool fL = vConeL[iObj] != 0;
+                bool fR = vConeR[iObj] != 0;
+                char Side = fL ? (fR ? 3 : 1) : (fR ? 2 : 0);
+                _vec_op_side[iOp] = Side;
+                if ( Side == 1 ) nL++;
+                else if ( Side == 2 ) nR++;
+                else if ( Side == 3 ) nB++;
+                else nN++;
+            }
+            LOG(1) << "CrossOnly: classified operators L=" << nL << " R=" << nR << " BOTH=" << nB << " NONE=" << nN;
+        }
+        else
+            LOG(1) << "CrossOnly: unable to derive LHS/RHS cones from miter; disabling cross filter.";
+    }
+
+    auto seed_pairs_for_indices = [&]( const vector<int>& vOpIdxs )
+    {
+        auto sig = [&]( int iObj, int iFanin )
+        {
+            int iFin = (iFanin == 0) ? Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, iObj)) : Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, iObj));
+            Wlc_Obj_t * pFin = Wlc_NtkObj(_pOrigNtk, iFin);
+            return std::make_pair( Wlc_ObjRange(pFin), Wlc_ObjIsSigned(pFin) );
+        };
+        auto sigOut = [&]( int iObj )
+        {
+            Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, iObj);
+            return std::make_pair( Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) );
+        };
+        for ( size_t i = 0; i < vOpIdxs.size(); ++i )
+        for ( size_t j = i + 1; j < vOpIdxs.size(); ++j )
+        {
+            int idx1  = vOpIdxs[i];
+            int idx2  = vOpIdxs[j];
+            int iObj1 = _vec_op_ids[idx1];
+            int iObj2 = _vec_op_ids[idx2];
+            Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, iObj1);
+            Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, iObj2);
+            if ( pObj1->Type != pObj2->Type )
+                continue;
+            if ( sigOut(iObj1) != sigOut(iObj2) )
+                continue;
+
+            bool fDirect = (sig(iObj1, 0) == sig(iObj2, 0)) && (sig(iObj1, 1) == sig(iObj2, 1));
+            bool fSwap   = (sig(iObj1, 0) == sig(iObj2, 1)) && (sig(iObj1, 1) == sig(iObj2, 0));
+            if ( fDirect ) {
+                UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 0);
+                if ( _allow_uif_pair(Pair) )
+                    _set_uif_pairs.insert( Pair );
+            }
+            if ( fSwap ) {
+                UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 1);
+                if ( _allow_uif_pair(Pair) )
+                    _set_uif_pairs.insert( Pair );
+            }
+        }
+    };
+
+    if ( params.nInitNearMults > 0 )
+    {
+        vector<pair<int, int> > vScoreIdx; // (seq distance from outputs, op-index in _vec_op_ids)
+        int nObjs = Wlc_NtkObjNumMax(_pOrigNtk);
+        vector<int> vDist(nObjs, -1);
+        queue<int> q;
+        Wlc_Obj_t * pPoT; int iPo;
+        Wlc_NtkForEachPo( _pOrigNtk, pPoT, iPo )
+        {
+            int iRoot = Wlc_ObjFaninId0(pPoT);
+            if ( iRoot > 0 && iRoot < nObjs && vDist[iRoot] == -1 )
+            {
+                vDist[iRoot] = 0;
+                q.push(iRoot);
+            }
+        }
+        while ( !q.empty() )
+        {
+            int iObj = q.front();
+            q.pop();
+            Wlc_Obj_t * pObjT = Wlc_NtkObj(_pOrigNtk, iObj);
+            int dNext = vDist[iObj] + 1;
+            if ( pObjT->Type == WLC_OBJ_FO )
+            {
+                Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT);
+                int iFi = Wlc_ObjId(_pOrigNtk, pFi);
+                if ( iFi > 0 && iFi < nObjs && (vDist[iFi] == -1 || dNext < vDist[iFi]) )
+                {
+                    vDist[iFi] = dNext;
+                    q.push(iFi);
+                }
+            }
+            int iFanin, k;
+            Wlc_ObjForEachFanin( pObjT, iFanin, k )
+            {
+                if ( iFanin <= 0 || iFanin >= nObjs )
+                    continue;
+                if ( vDist[iFanin] == -1 || dNext < vDist[iFanin] )
+                {
+                    vDist[iFanin] = dNext;
+                    q.push(iFanin);
+                }
+            }
+        }
+
+        for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
+        {
+            int iObj = _vec_op_ids[i];
+            if ( Wlc_NtkObj(_pOrigNtk, iObj)->Type != WLC_OBJ_ARI_MULTI )
+                continue;
+            if ( iObj <= 0 || iObj >= nObjs )
+                continue;
+            if ( vDist[iObj] < 0 )
+                continue;
+            vScoreIdx.push_back( { vDist[iObj], (int)i } );
+        }
+        sort( vScoreIdx.begin(), vScoreIdx.end(),
+              []( const pair<int,int>& a, const pair<int,int>& b )
+              { return a.first != b.first ? a.first < b.first : a.second < b.second; } );
+        vector<int> vSeedOps;
+        size_t nTake = Abc_MinInt( (int)vScoreIdx.size(), (int)params.nInitNearMults );
+        vSeedOps.reserve( nTake );
+        for ( size_t i = 0; i < nTake; ++i )
+            vSeedOps.push_back( vScoreIdx[i].second );
+        sort( vSeedOps.begin(), vSeedOps.end() );
+
+        size_t nBefore = _set_uif_pairs.size();
+        seed_pairs_for_indices( vSeedOps );
+        if ( _set_uif_pairs.size() > nBefore ) {
+            LOG(1) << "InitNear: pre-seeded " << (_set_uif_pairs.size() - nBefore)
+                   << " UIF pairs among " << vSeedOps.size() << " closest multipliers (limit = " << params.nInitNearMults << ")";
+        }
+    }
+
+    if ( params.nInitAllPairsLimit > 0 && _vec_op_ids.size() <= params.nInitAllPairsLimit )
+    {
+        vector<int> vAllOps;
+        vAllOps.reserve( _vec_op_ids.size() );
+        for ( size_t i = 0; i < _vec_op_ids.size(); ++i )
+            vAllOps.push_back( (int)i );
+        size_t nBefore = _set_uif_pairs.size();
+        seed_pairs_for_indices( vAllOps );
+        if ( _set_uif_pairs.size() > nBefore ) {
+            LOG(1) << "InitAllPairs: pre-seeded " << (_set_uif_pairs.size() - nBefore)
+                   << " UIF pairs (ops = " << _vec_op_ids.size() << ", limit = " << params.nInitAllPairsLimit << ")";
+        }
+    }
 
     _p_sim_mgr.reset(new SimUifPairFinder(_pOrigNtk, &_vec_op_ids));
     _p_cex_mgr.reset(new CexUifPairFinder(_pOrigNtk, &_vec_op_ids));
 
-    LogT::loglevel = params.iVerbosity;
-
     struct timeval now;
     gettimeofday(&now, NULL);
     _timeout.tv_sec = now.tv_sec + params.nTimeout;
@@ -1122,6 +1362,8 @@ void UfarManager::FindUifPairsUsingSim() {
 
     set<UIF_PAIR> set_new_pairs;
     for(auto& x:_set_uif_sim_pairs) {
+        if ( !_allow_uif_pair(x) )
+            continue;
         auto res = _set_uif_pairs.insert(x);
         if(res.second)
             set_new_pairs.insert(x);
@@ -1149,6 +1391,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) {
     } else {
         _p_cex_mgr->FindUifPairsBasic(cex_po_values, params.nSeqLookBack, set_found_pairs);
     }
+    if ( params.fCrossOnly && _fCrossReady )
+    {
+        for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
+            if ( !_allow_uif_pair(*it) )
+                it = set_found_pairs.erase(it);
+            else
+                ++it;
+    }
     if(log_level() >= 3) print_pairs(set_found_pairs);
 
     if(params.fPbaUif && !set_found_pairs.empty()) {
@@ -1171,6 +1421,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) {
         }
     }
 
+    if ( params.fCrossOnly && _fCrossReady )
+    {
+        for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); )
+            if ( !_allow_uif_pair(*it) )
+                it = set_found_pairs.erase(it);
+            else
+                ++it;
+    }
     for(auto& x : set_found_pairs) _set_uif_pairs.insert(x);
 
     gettimeofday(&t2, NULL);
@@ -1403,7 +1661,7 @@ int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) {
         }
     }
     */
-    ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId);
+    ret = verify_model(pCurrent, ppCex, &params.fileName, &params.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId, &params.solverSetting, (int)params.nTimeout);
     Wlc_NtkFree(pCurrent);
 
     gettimeofday(&t2, NULL);
@@ -1447,9 +1705,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
         LOG(1) << "Grey: [Total] = " << setprecision(4) << stat << " (" << _vec_op_greyness.size() << ")";
     };
     auto print_stat = [&]() {
+        unsigned nWhiteBoxes = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
+        if (profile.nMaxUifPairs < _set_uif_pairs.size())
+            profile.nMaxUifPairs = _set_uif_pairs.size();
+        if (profile.nMaxWhiteBoxes < nWhiteBoxes)
+            profile.nMaxWhiteBoxes = nWhiteBoxes;
         gettimeofday(&curTime, NULL);
         elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0;
-        snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4lu White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false), _set_uif_pairs.size(), elapsedTime);
+        snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4u White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, nWhiteBoxes, _set_uif_pairs.size(), elapsedTime);
         LOG(1) << buffer << _get_profile_uf_wb();
         dump_grey_stat();
         if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut);
@@ -1491,18 +1754,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
                 Wlc_NtkFree(pCurrent);
                 ret = 0;
             } else {
+                profile.nVerifyCalls++;
                 ret = VerifyCurrentAbstraction(&mem.pCex);
             }
 
             if (ret ==  0) { // SAT
+                profile.nSatCalls++;
                 if ( Ufar_ShouldStop(params) )
                     return -1;
                 // GetOperatorsInCex(mem.pCex);
-                if (verify_cex_on_original(_pOrigNtk, mem.pCex)) {
+                timeval tCheck1, tCheck2;
+                gettimeofday(&tCheck1, NULL);
+                bool fRealCex = verify_cex_on_original(_pOrigNtk, mem.pCex);
+                gettimeofday(&tCheck2, NULL);
+                profile.tCexCheckOrig += elapsed_time_usec(tCheck1, tCheck2);
+                if (fRealCex) {
+                    profile.nRealCex++;
                     PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names);
                     return 0;
                 }
+                profile.nSpuriousCex++;
                 unsigned n_before = _set_uif_pairs.size();
+                set<UIF_PAIR> set_before = _set_uif_pairs;
 
                 FindUifPairsUsingCex(mem.pCex, &mem.pCex2);
                 if ( Ufar_ShouldStop(params) )
@@ -1534,17 +1807,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
                     }
                 }
 
+                if (_set_uif_pairs.size() > n_before)
+                    profile.nUifPairsAdded += (_set_uif_pairs.size() - n_before);
+                if (_set_uif_pairs.size() > n_before) {
+                    for (const auto& x : _set_uif_pairs) {
+                        if (set_before.find(x) == set_before.end() && _is_mul_mul_pair(x))
+                            profile.nUifMulMulPairsAdded++;
+                    }
+                }
                 ++n_iter_uif;
+                profile.nIterUif++;
                 print_stat();
 
                 if(_set_uif_pairs.size() > params.nConstraintLimit)
                     return -1;
             } else if (ret == 1) { // UNSAT
+                profile.nUnsatCalls++;
                 //_shrink_final_abstraction();
                 //print_stat();
                 return 1;
 
             } else {
+                profile.nUnknownCalls++;
                 return -1;
 
             }
@@ -1552,9 +1836,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
 
         if ( Ufar_ShouldStop(params) )
             return -1;
+        unsigned nWhiteBoxesBefore = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
         DetermineWhiteBoxes(mem.pCex);
+        unsigned nWhiteBoxesAfter  = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false);
+        if (nWhiteBoxesAfter > nWhiteBoxesBefore)
+            profile.nWbAdded += (nWhiteBoxesAfter - nWhiteBoxesBefore);
 
         ++n_iter_wb;
+        profile.nIterWb++;
         print_stat();
     }
     return -1;
@@ -1573,6 +1862,31 @@ void UfarManager::_massage_state_b() {
 }
 
 
+bool UfarManager::_is_mul_mul_pair(const UIF_PAIR& x) const {
+    if (!_pOrigNtk)
+        return false;
+    if (x.first.idx >= _vec_op_ids.size() || x.second.idx >= _vec_op_ids.size())
+        return false;
+    int obj1 = _vec_op_ids[x.first.idx];
+    int obj2 = _vec_op_ids[x.second.idx];
+    Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, obj1);
+    Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, obj2);
+    return pObj1 && pObj2 && pObj1->Type == WLC_OBJ_ARI_MULTI && pObj2->Type == WLC_OBJ_ARI_MULTI;
+}
+
+bool UfarManager::_allow_uif_pair(const UIF_PAIR& x) const {
+    if ( !params.fCrossOnly || !_fCrossReady )
+        return true;
+    if ( x.first.idx < 0 || x.second.idx < 0 )
+        return false;
+    if ( x.first.idx >= (int)_vec_op_side.size() || x.second.idx >= (int)_vec_op_side.size() )
+        return false;
+    char s1 = _vec_op_side[x.first.idx];
+    char s2 = _vec_op_side[x.second.idx];
+    return (s1 == 1 && s2 == 2) || (s1 == 2 && s2 == 1);
+}
+
+
 string UfarManager::_get_profile_uf_wb() {
     if (log_level() <= 4) return "";
     unsigned num_full_white = 0;
@@ -1625,6 +1939,9 @@ void UfarManager::DumpParams() const {
     unsigned n_setw = 15;
     cout << "Parameters : " << endl;
     cout << "     " << setw(n_setw) << left << "cexmin" << " : " << (params.fCexMin ? "yes" : "no") << endl;
+    cout << "     " << setw(n_setw) << left << "allwb" << " : " << (params.fAllWb ? "yes" : "no") << endl;
+    cout << "     " << setw(n_setw) << left << "crossonly" << " : " << (params.fCrossOnly ? "yes" : "no") << endl;
+    cout << "     " << setw(n_setw) << left << "initnear" << " : " << params.nInitNearMults << endl;
     cout << "     " << setw(n_setw) << left << "iLogLevel" << " : " << params.iVerbosity << endl;
 }
 
diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h
index 31b91ef40..ad17d8474 100755
--- a/src/opt/ufar/UfarMgr.h
+++ b/src/opt/ufar/UfarMgr.h
@@ -42,6 +42,9 @@ typedef struct Gia_Man_t_ Gia_Man_t;
 
 namespace UFAR {
 
+void Ufar_ResetOrigCexStats();
+void Ufar_GetOrigCexStats(unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec);
+
 using VecVecInt = std::vector<std::vector<int> >;
 using VecVecStr = std::vector<std::vector<std::string> >;
 using VecChar = std::vector<char>;
@@ -72,6 +75,8 @@ class UfarManager {
             bool     fGrey;
             float    nGrey;
             bool     fNorm;
+            bool     fAllWb;
+            bool     fCrossOnly;
             bool     fSuper_prove;
             bool     fSimple;
             bool     fSyn;
@@ -79,23 +84,43 @@ class UfarManager {
             int      iOneWb;
             int      iExp;
             unsigned nConstraintLimit;
+            unsigned nInitAllPairsLimit;
+            unsigned nInitNearMults;
             unsigned iVerbosity;
             unsigned nSeqLookBack;
             unsigned nTimeout;
             std::string simSetting;
             std::string parSetting;
+            std::string solverSetting;
             std::string fileName;
             std::string fileAbs;
             std::string fileStatesOut;
             std::string fileStatesIn;
         };
         struct Profile {
-            Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0) {}
+            Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0), tCexCheckOrig(0),
+                        nVerifyCalls(0), nSatCalls(0), nUnsatCalls(0), nUnknownCalls(0),
+                        nRealCex(0), nSpuriousCex(0), nIterUif(0), nIterWb(0),
+                        nUifPairsAdded(0), nUifMulMulPairsAdded(0), nWbAdded(0), nMaxUifPairs(0), nMaxWhiteBoxes(0) {}
             unsigned tBLSolver;
             unsigned tUifRefine;
             unsigned tWbRefine;
             unsigned tUifSim;
             unsigned tGbRefine;
+            unsigned tCexCheckOrig;
+            unsigned nVerifyCalls;
+            unsigned nSatCalls;
+            unsigned nUnsatCalls;
+            unsigned nUnknownCalls;
+            unsigned nRealCex;
+            unsigned nSpuriousCex;
+            unsigned nIterUif;
+            unsigned nIterWb;
+            unsigned nUifPairsAdded;
+            unsigned nUifMulMulPairsAdded;
+            unsigned nWbAdded;
+            unsigned nMaxUifPairs;
+            unsigned nMaxWhiteBoxes;
         };
 
         UfarManager();
@@ -132,6 +157,8 @@ class UfarManager {
         void        _perform_proof_based_grey_boxing(Abc_Cex_t * pCex);
         void        _perform_cex_based_white_boxing();
         std::string _get_profile_uf_wb();
+        bool        _is_mul_mul_pair(const UIF_PAIR& x) const;
+        bool        _allow_uif_pair(const UIF_PAIR& x) const;
         void        _massage_state_b();
         void        _dump_states(const std::string& file);
         void        _read_states(const std::string& file);
@@ -143,6 +170,7 @@ class UfarManager {
 
         std::vector<int>                _vec_op_ids;
         std::vector<bool>               _vec_op_blackbox_marks;
+        std::vector<char>               _vec_op_side; // 0=unknown, 1=L-only, 2=R-only, 3=both
         std::vector<std::vector<int> >  _vec_vec_op_ffs;
         std::vector<Greyness>           _vec_op_greyness;
 
@@ -156,6 +184,7 @@ class UfarManager {
         std::unique_ptr<CexUifPairFinder>  _p_cex_mgr;
 
         std::ostringstream       _oss;
+        bool                     _fCrossReady;
 
         struct timespec          _timeout;
 };
diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp
index 9c2a1da85..b0cb5bd15 100755
--- a/src/opt/untk/NtkNtk.cpp
+++ b/src/opt/untk/NtkNtk.cpp
@@ -11,12 +11,18 @@
 #include <unistd.h>
 #endif
 #include <fstream>
+#include <cstdio>
+#include <cstdlib>
+#include <ctime>
+#include <algorithm>
+#include <cctype>
 
 #include <base/wlc/wlc.h>
 #include <sat/bmc/bmc.h>
 #include <proof/pdr/pdr.h>
 #include <proof/fraig/fraig.h>
 #include <aig/gia/giaAig.h>
+#include <base/io/ioAbc.h>
 
 #include "opt/util/util.h"
 #include "opt/ufar/UfarPth.h"
@@ -1250,11 +1256,77 @@ static void readCexFromFile(int& ret, FILE * file, Abc_Cex_t ** ppCex, int nOrig
     }
 }
 
-int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId) {
+static inline bool is_solver_cmd_defined(const string* pSolverSetting) {
+    return pSolverSetting && !pSolverSetting->empty() && *pSolverSetting != "none";
+}
+
+static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string& solverCmd, int nRuntimeLimitSec )
+{
+    const char * pAigFile = "file.aig";
+    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;
+    if ( nRuntimeLimitSec > 0 )
+        command += " " + to_string(nRuntimeLimitSec);
+    command += " > log.txt 2>&1";
+    LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
+    int res = system( command.c_str() );
+    std::remove( pAigFile );
+    return res;
+}
+
+static inline int read_external_status_unsat_first_line()
+{
+    ifstream ifs("status.txt", std::ifstream::in);
+    if ( !ifs )
+        return -1;
+    int firstLine = -1;
+    ifs >> firstLine;
+    if ( ifs && firstLine == 0 )
+        return 1;
+    return -1;
+}
+
+static inline int read_external_result_from_log_last_line()
+{
+    ifstream ifs("log.txt", std::ifstream::in);
+    if ( !ifs )
+        return -1;
+    string line, last;
+    auto trim = []( 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();
+    };
+    while ( getline(ifs, line) )
+    {
+        trim(line);
+        if ( !line.empty() )
+            last = line;
+    }
+    if ( last.empty() )
+        return -1;
+    transform( last.begin(), last.end(), last.begin(),
+               []( unsigned char c ){ return (char)toupper(c); } );
+    if ( last.find("UNSAT") != string::npos )
+        return 1;
+    if ( last.find("SAT") != string::npos )
+        return 0;
+    if ( last.find("UNKNOWN") != string::npos || last.find("UNDECIDED") != string::npos )
+        return -1;
+    return -1;
+}
+
+int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId, const string* pSolverSetting, int nUfarTimeoutSec) {
     if ( pFuncStop && pFuncStop(RunId) )
         return -1;
     if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 )
-        return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId );
+        return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId, pSolverSetting, nUfarTimeoutSec );
     
     if(*ppCex) {
         Abc_CexFree(*ppCex);
@@ -1275,7 +1347,7 @@ int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName,
 }
 
 
-int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId) {
+int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId, const string* pSolverSetting, int nRuntimeLimitSec) {
     if ( pFuncStop && pFuncStop(RunId) )
         return -1;
     if(*ppCex) {
@@ -1319,6 +1391,27 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam
         }
     } else {
         auto runPDR = [&](FILE * file){
+            if ( is_solver_cmd_defined(pSolverSetting) )
+            {
+                run_external_solver_on_aig( pAbcNtk, *pSolverSetting, nRuntimeLimitSec );
+                int extStatus = read_external_result_from_log_last_line();
+                if ( extStatus == -1 )
+                    extStatus = read_external_status_unsat_first_line();
+                if ( extStatus == 1 )
+                    LOG(1) << "UFAR external solver result (UNSAT) available. Skipping PDR.";
+                else
+                    LOG(1) << "UFAR external solver result not usable (log/status not UNSAT). Calling PDR.";
+                if ( extStatus == 1 )
+                {
+                    writeCexToFile(1, file, NULL);
+                    return 1;
+                }
+                if ( pFuncStop && pFuncStop(RunId) )
+                {
+                    writeCexToFile(-1, file, NULL);
+                    return -1;
+                }
+            }
             Pdr_Par_t PdrPars, *pPdrPars = &PdrPars;
             Pdr_ManSetDefaultParams(pPdrPars);
             pPdrPars->nConfLimit = 0;
diff --git a/src/opt/untk/NtkNtk.h b/src/opt/untk/NtkNtk.h
index 85d9ac935..07b1c12f0 100755
--- a/src/opt/untk/NtkNtk.h
+++ b/src/opt/untk/NtkNtk.h
@@ -136,8 +136,8 @@ void        PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vector<s
 
 unsigned    compute_bit_level_pi_num(Wlc_Ntk_t * pNtk);
 
-int         verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, struct timespec * timeout = NULL, int (*pFuncStop)(int) = NULL, int RunId = -1);
-int         bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, int (*pFuncStop)(int) = NULL, int RunId = -1);
+int         verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, struct timespec * timeout = NULL, int (*pFuncStop)(int) = NULL, int RunId = -1, const std::string* pSolverSetting = NULL, int nUfarTimeoutSec = -1);
+int         bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const std::string* pFileName = NULL, const std::string* pParSetting = NULL, bool fSyn = false, int (*pFuncStop)(int) = NULL, int RunId = -1, const std::string* pSolverSetting = NULL, int nRuntimeLimitSec = -1);
 
 Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk);
 
diff --git a/src/opt/util/util.cpp b/src/opt/util/util.cpp
index fa80bebd9..221d1a6b2 100644
--- a/src/opt/util/util.cpp
+++ b/src/opt/util/util.cpp
@@ -48,7 +48,32 @@ bool OptMgr::Parse(int argc, char * argv[]) {
         if(!opt.isBool()) {
             if (i + 1 == argc)
                 return false;
-            opt._val = argv[++i];
+            string val = argv[++i];
+            if ( !val.empty() && (val[0] == '"' || val[0] == '\'') )
+            {
+                char q = val[0];
+                bool fClosed = val.size() >= 2 && val.back() == q;
+                if ( fClosed )
+                    val = val.substr(1, val.size() - 2);
+                else
+                {
+                    val.erase(0, 1);
+                    while ( i + 1 < argc )
+                    {
+                        string next = argv[++i];
+                        if ( !next.empty() && next.back() == q )
+                        {
+                            val += " " + next.substr(0, next.size() - 1);
+                            fClosed = true;
+                            break;
+                        }
+                        val += " " + next;
+                    }
+                    if ( !fClosed )
+                        return false;
+                }
+            }
+            opt._val = val;
         }
     }
 

From 7ae0f4966a68ba3190b03a16810ae3daf23d14c0 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 8 Mar 2026 12:04:25 -0700
Subject: [PATCH 6/6] Adding gla to sprove.

---
 src/base/abci/abc.c      |  2 +-
 src/proof/abs/abs.h      |  3 ++-
 src/proof/abs/absGla.c   | 10 +++++++++-
 src/proof/abs/absUtil.c  |  3 ++-
 src/proof/cec/cecProve.c | 36 +++++++++++++++++++++++++++++++++---
 5 files changed, 47 insertions(+), 7 deletions(-)

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f1bef5e23..63847c88b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -51398,7 +51398,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;
-    int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
+    int c, nProcs = 6, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF )
     {
diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h
index 1c31e7cc6..782afebdf 100644
--- a/src/proof/abs/abs.h
+++ b/src/proof/abs/abs.h
@@ -74,6 +74,8 @@ struct Abs_Par_t_
     char *         pFileVabs;          // dumps the abstracted model into this file
     int            fVerbose;           // verbose flag
     int            fVeryVerbose;       // print additional information
+    int            RunId;              // id in this run
+    int            (*pFuncStop)(int);  // callback to terminate
     int            iFrame;             // the number of frames covered
     int            iFrameProved;       // the number of frames proved
     int            nFramesNoChange;    // the number of last frames without changes
@@ -174,4 +176,3 @@ ABC_NAMESPACE_HEADER_END
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 75f991d3b..9f1a8a31e 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1576,6 +1576,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
     for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
     {
         int nAbsOld;
+        if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
+            goto finish;
         // remember the timeframe
         p->pPars->iFrame = -1;
         // create new SAT solver
@@ -1585,6 +1587,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         // unroll the circuit
         for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
         {
+            if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
+                goto finish;
             // remember current limits
             int nConflsBeg = sat_solver2_nconflicts(p->pSat);
             int nAbs       = Vec_IntSize(p->vAbs);
@@ -1618,6 +1622,11 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
             nVarsOld = p->nSatVars;
             for ( c = 0; ; c++ )
             {
+                if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
+                {
+                    Status = l_Undef;
+                    goto finish;
+                }
                 // consider the special case when the target literal is implied false
                 // by implications which happened as a result of previous refinements
                 // note that incremental UNSAT core cannot be computed because there is no learned clauses
@@ -1898,4 +1907,3 @@ finish:
 
 
 ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/abs/absUtil.c b/src/proof/abs/absUtil.c
index 286d1091b..d0d85ae41 100644
--- a/src/proof/abs/absUtil.c
+++ b/src/proof/abs/absUtil.c
@@ -59,6 +59,8 @@ void Abs_ParSetDefaults( Abs_Par_t * p )
     p->fUseRollback       =      0;   // use rollback to the starting number of frames
     p->fPropFanout        =      1;   // propagate fanouts during refinement
     p->fVerbose           =      0;   // verbose flag
+    p->RunId              =     -1;   // id in this run
+    p->pFuncStop          =   NULL;   // callback to terminate
     p->iFrame             =     -1;   // the number of frames covered 
     p->iFrameProved       =     -1;   // the number of frames proved
     p->nFramesNoChangeLim =      2;   // the number of frames without change to dump abstraction
@@ -254,4 +256,3 @@ int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
 
 
 ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c
index 017296540..c3ed1fad7 100644
--- a/src/proof/cec/cecProve.c
+++ b/src/proof/cec/cecProve.c
@@ -26,6 +26,7 @@
 #include "proof/pdr/pdr.h"
 #include "proof/cec/cec.h"
 #include "proof/ssw/ssw.h"
+#include "proof/abs/abs.h"
 
 
 #ifdef ABC_USE_PTHREADS
@@ -66,6 +67,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
 #define PAR_ENGINE_UFAR 6
 #define PAR_ENGINE_SCORR1 7
 #define PAR_ENGINE_SCORR2 8
+#define PAR_ENGINE_GLA 9
 struct Par_Share_t_
 {
     volatile int       fSolved;
@@ -90,6 +92,7 @@ typedef struct Cec_ScorrStop_t_
     abctime TimeToStop;
 } Cec_ScorrStop_t;
 static volatile Par_Share_t * g_pUfarShare = NULL;
+static volatile Par_Share_t * g_pGlaShare = NULL;
 static inline const char * Cec_SolveEngineName( int iEngine )
 {
     if ( iEngine == 0 ) return "rar";
@@ -101,6 +104,7 @@ static inline const char * Cec_SolveEngineName( int iEngine )
     if ( iEngine == PAR_ENGINE_UFAR ) return "ufar";
     if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new";
     if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old";
+    if ( iEngine == PAR_ENGINE_GLA ) return "gla-q";
     return "unknown";
 }
 static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
@@ -128,6 +132,11 @@ static int Cec_SProveStopUfar( int RunId )
     (void)RunId;
     return g_pUfarShare && g_pUfarShare->fSolved != 0;
 }
+static int Cec_SProveStopGla( int RunId )
+{
+    (void)RunId;
+    return g_pGlaShare && g_pGlaShare->fSolved != 0;
+}
 static int Cec_ScorrStop( void * pUser )
 {
     Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser;
@@ -177,7 +186,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
 {
     abctime clk = Abc_Clock();   
     int RetValue = -1;
-    if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 )
+    if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 )
     {
         if ( fVerbose )
             printf( "Engine %d skipped because the current miter is combinational.\n", iEngine );
@@ -294,6 +303,22 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
             g_pUfarShare = NULL;
         }
     }
+    else if ( iEngine == PAR_ENGINE_GLA )
+    {
+        if ( Gia_ManPoNum(p) != 1 )
+            return -1;
+        Abs_Par_t Pars, * pPars = &Pars;
+        Abs_ParSetDefaults( pPars );
+        pPars->nTimeOut = nTimeOut;
+        pPars->fCallProver = 1; // emulate "&gla -q"
+        pPars->fVerbose = 0;
+        pPars->fVeryVerbose = 0;
+        pPars->RunId = 0;
+        pPars->pFuncStop = Cec_SProveStopGla;
+        g_pGlaShare = pThData ? pThData->pShare : NULL;
+        RetValue = Gia_ManPerformGla( p, pPars );
+        g_pGlaShare = NULL;
+    }
     else assert( 0 );
     //while ( Abc_Clock() < clkStop );
     if ( pThData && pThData->pShare && RetValue != -1 )
@@ -379,7 +404,12 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
     {
         ThData[i].p        = Gia_ManDup(p);
         Cec_CopyGiaName( p, ThData[i].p );
-        ThData[i].iEngine  = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
+        if ( fUseUif && i == nWorkers - 1 )
+            ThData[i].iEngine = PAR_ENGINE_UFAR;
+        else if ( !fUseUif && nWorkers == 6 && i == 5 )
+            ThData[i].iEngine = PAR_ENGINE_GLA;
+        else
+            ThData[i].iEngine = i;
         ThData[i].nTimeOut = nTimeOut;
         ThData[i].fWorking = 0;
         ThData[i].Result   = -1;
@@ -427,7 +457,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
         printf( "Processes = %d   TimeOut = %d sec   Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
     fflush( stdout );
 
-    assert( nProcs == 3 || nProcs == 5 );
+    assert( nProcs == 3 || nProcs == 5 || nProcs == 6 );
     assert( nWorkers <= PAR_THR_MAX );
     Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share );