Version abc60611

19 files changed, 340 insertions, 164 deletions

diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index 5d2547ea..a0d63ce9 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -64,9 +64,11 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 //typedef int                   bool;
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef struct Aig_Param_t_     Aig_Param_t;
 typedef struct Aig_Man_t_       Aig_Man_t;
@@ -215,7 +217,7 @@ struct Aig_SimInfo_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Aig_BitWordNum( int nBits )            { return nBits/32 + ((nBits%32) > 0);       }
+static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);     }
 static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
 static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));             }
 static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));             }
diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c
index 525d4a14..03781180 100644
--- a/src/sat/aig/fraigCore.c
+++ b/src/sat/aig/fraigCore.c
@@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
     // solve the miter
     clk = clock();
     pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
-    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit );
+    status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
index 92a39f0a..cb8d03e0 100644
--- a/src/sat/aig/rwrTruth.c
+++ b/src/sat/aig/rwrTruth.c
@@ -167,7 +167,7 @@ void Aig_TruthCount( Aig_Truth_t * p )
 ***********************************************************************/
 static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
 {
-    return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size));
+    return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size));
 }
 
 /**Function*************************************************************
@@ -183,7 +183,7 @@ static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size )
 ***********************************************************************/
 static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part )
 {
-    p[Start/5] |= (Part << (Start%32));
+    p[Start/5] |= (Part << (Start&31));
 }
 
 /**Function*************************************************************
@@ -254,7 +254,7 @@ DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int n
     }
     if ( nVars == 5 )
     {
-        unsigned * pWord = pTruth + Shift/32;
+        unsigned * pWord = pTruth + (Shift>>5);
         assert( Shift % 32 == 0 );
         if ( *pWord == 0 )
             return Cudd_ReadLogicZero(dd);
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index e1b1bb2a..832bc0cf 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -158,7 +158,7 @@ int * solver_get_model( solver * p, int * pVars, int nVars )
     for ( i = 0; i < nVars; i++ )
     {
         assert( pVars[i] >= 0 && pVars[i] < p->size );
-        pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True);
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
     }
     return pModel;    
 }
@@ -188,6 +188,28 @@ void Asat_SatPrintStats( FILE * pFile, solver * p )
         (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the preferred variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars)
+{
+    int i;
+    assert( s->pPrefVars == NULL );
+    for ( i = 0; i < nPrefVars; i++ )
+        assert( pPrefVars[i] < s->size );
+    s->pPrefVars = pPrefVars;
+    s->nPrefVars = nPrefVars;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/asat60525.zip b/src/sat/asat/asat60525.zip
new file mode 100644
index 00000000..b8361af1
--- /dev/null
+++ b/src/sat/asat/asat60525.zip
diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c
index 1def6a37..8e673cc9 100644
--- a/src/sat/asat/jfront.c
+++ b/src/sat/asat/jfront.c
@@ -95,7 +95,7 @@ static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar );
 
 // iterator through the adjacent variables
 #define Asat_JVarForEachFanio( p, pVar, pFan, i )               \
-    for ( i = 0; (i < pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ )
+    for ( i = 0; (i < (int)pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ )
 
 extern void Asat_JManAssign( Asat_JMan_t * p, int Var );
 
@@ -223,7 +223,7 @@ int Asat_JManCheck( Asat_JMan_t * p )
 //        assert( i != pVar->nFans );
 //        if ( i == pVar->nFans )
 //            return 0;
-        if ( i == pVar->nFans )
+        if ( i == (int)pVar->nFans )
             Counter++;
     }
     if ( Counter > 0 )
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 6d76d890..548abd1d 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "solver.h"
 
-//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
+#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
 
 //=================================================================================================
 // Simple (var/literal) helpers:
@@ -96,14 +96,14 @@ static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[
 //=================================================================================================
 // Encode literals in clause pointers:
 
-clause* clause_from_lit (lit l)     { return (clause*)(l + l + 1);        }
-bool    clause_is_lit   (clause* c) { return ((unsigned int)c & 1);       }
-lit     clause_read_lit (clause* c) { return (lit)((unsigned int)c >> 1); }
+clause* clause_from_lit (lit l)     { return (clause*)(((unsigned long)l) + ((unsigned long)l) + 1);        }
+bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);       }
+lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
 
 //=================================================================================================
 // Simple helpers:
 
-static inline int     solver_dlevel(solver* s)    { return vec_size(&s->trail_lim); }
+static inline int     solver_dlevel(solver* s)    { return veci_size(&s->trail_lim); }
 static inline vec*    solver_read_wlist     (solver* s, lit l){ return &s->wlists[l]; }
 static inline void    vec_remove(vec* v, void* e)
 {
@@ -124,7 +124,7 @@ static inline void order_update(solver* s, int v) // updateorder
 //    int clk = clock();
     int*    orderpos = s->orderpos;
     double* activity = s->activity;
-    int*    heap     = (int*)vec_begin(&s->order);
+    int*    heap     = veci_begin(&s->order);
     int     i        = orderpos[v];
     int     x        = heap[i];
     int     parent   = (i - 1) / 2;
@@ -151,8 +151,8 @@ static inline void order_unassigned(solver* s, int v) // undoorder
 //    int clk = clock();
     int* orderpos = s->orderpos;
     if (orderpos[v] == -1){
-        orderpos[v] = vec_size(&s->order);
-        vec_push(&s->order,(void*)v);
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
         order_update(s,v);
     }
 //    s->timeUpdate += clock() - clk;
@@ -161,12 +161,23 @@ static inline void order_unassigned(solver* s, int v) // undoorder
 static int  order_select(solver* s, float random_var_freq) // selectvar
 {
 //    int clk = clock();
+    static int Counter = 0;
     int*    heap;
     double* activity;
     int*    orderpos;
 
     lbool* values = s->assigns;
 
+    // The first decisions
+    if ( s->pPrefVars && s->nPrefDecNum < s->nPrefVars )
+    {
+        int i;
+        s->nPrefDecNum++;
+        for ( i = 0; i < s->nPrefVars; i++ )
+            if ( values[s->pPrefVars[i]] == l_Undef )
+                return s->pPrefVars[i];
+    }
+
     // Random decision:
     if (drand(&s->random_seed) < random_var_freq){
         int next = irand(&s->random_seed,s->size);
@@ -177,17 +188,17 @@ static int  order_select(solver* s, float random_var_freq) // selectvar
 
     // Activity based decision:
 
-    heap     = (int*)vec_begin(&s->order);
+    heap     = veci_begin(&s->order);
     activity = s->activity;
     orderpos = s->orderpos;
 
 
-    while (vec_size(&s->order) > 0){
+    while (veci_size(&s->order) > 0){
         int    next  = heap[0];
-        int    size  = vec_size(&s->order)-1;
+        int    size  = veci_size(&s->order)-1;
         int    x     = heap[size];
 
-        vec_resize(&s->order,size);
+        veci_resize(&s->order,size);
 
         orderpos[next] = -1;
 
@@ -300,7 +311,10 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
     assert(((unsigned int)c & 1) == 0);
 
     for (i = 0; i < size; i++)
+    {
+        assert(begin[i] >= 0);
         c->lits[i] = begin[i];
+    }
 
     if (learnt)
         *((float*)&c->lits[size]) = 0.0;
@@ -328,11 +342,11 @@ static void clause_remove(solver* s, clause* c)
     lit* lits = clause_begin(c);
     assert(neg(lits[0]) < s->size*2);
     assert(neg(lits[1]) < s->size*2);
+    assert(lits[0] < s->size*2);
 
     //vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)c);
     //vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)c);
 
-    assert(lits[0] < s->size*2);
     vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
     vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
 
@@ -399,8 +413,8 @@ static void solver_setnvars(solver* s,int n)
         s->levels   [var] = 0;
         s->tags     [var] = l_Undef;
 
-        assert(vec_size(&s->order) == var);
-        vec_push(&s->order,(void*)var);
+        assert(veci_size(&s->order) == var);
+        veci_push(&s->order,var);
         order_update(s,var);
     }
 
@@ -413,20 +427,19 @@ static inline bool enqueue(solver* s, lit l, clause* from)
     lbool* values = s->assigns;
     int    v      = lit_var(l);
     lbool  val    = values[v];
+    lbool sig = !lit_sign(l); sig += sig - 1;
 #ifdef VERBOSEDEBUG
     printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
 #endif
-
-    lbool sig = !lit_sign(l); sig += sig - 1;
     if (val != l_Undef){
         return val == sig;
     }else{
         // New fact -- store it.
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
 #ifdef VERBOSEDEBUG
         printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
 #endif
-        int*     levels  = s->levels;
-        clause** reasons = s->reasons;
 
         values [v] = sig;
         levels [v] = solver_dlevel(s);
@@ -448,7 +461,7 @@ static inline void assume(solver* s, lit l){
 #ifdef VERBOSEDEBUG
     printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
 #endif
-    vec_push(&s->trail_lim,(void*)s->qtail);
+    veci_push(&s->trail_lim,s->qtail);
     enqueue(s,l,(clause*)0);
 }
 
@@ -466,7 +479,7 @@ static inline void solver_canceluntil(solver* s, int level) {
     trail   = s->trail;
     values  = s->assigns;
     reasons = s->reasons;
-    bound   = ((int*)vec_begin(&s->trail_lim))[level];
+    bound   = veci_begin(&s->trail_lim)[level];
 
     for (c = s->qtail-1; c >= bound; c--) {
         int     x  = lit_var(trail[c]);
@@ -482,23 +495,23 @@ static inline void solver_canceluntil(solver* s, int level) {
             order_unassigned( s, lit_var(trail[c]) );
 
     s->qhead = s->qtail = bound;
-    vec_resize(&s->trail_lim,level);
+    veci_resize(&s->trail_lim,level);
 }
 
-static void solver_record(solver* s, vec* cls)
+static void solver_record(solver* s, veci* cls)
 {
-    lit*    begin = (lit*)vec_begin(cls);
-    lit*    end   = begin + vec_size(cls);
-    clause* c     = (vec_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
     enqueue(s,*begin,c);
 
-    assert(vec_size(cls) > 0);
+    assert(veci_size(cls) > 0);
 
     if (c != 0) {
         vec_push(&s->learnts,(void*)c);
         act_clause_bump(s,c);
         s->solver_stats.learnts++;
-        s->solver_stats.learnts_literals += vec_size(cls);
+        s->solver_stats.learnts_literals += veci_size(cls);
     }
 }
 
@@ -525,18 +538,18 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
     lbool*   tags    = s->tags;
     clause** reasons = s->reasons;
     int*     levels  = s->levels;
-    int      top     = vec_size(&s->tagged);
+    int      top     = veci_size(&s->tagged);
 
     assert(lit_var(l) >= 0 && lit_var(l) < s->size);
     assert(reasons[lit_var(l)] != 0);
-    vec_resize(&s->stack,0);
-    vec_push(&s->stack,(void*)lit_var(l));
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
 
-    while (vec_size(&s->stack) > 0){
+    while (veci_size(&s->stack) > 0){
         clause* c;
-        int v = (int)vec_begin(&s->stack)[vec_size(&s->stack)-1];
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
         assert(v >= 0 && v < s->size);
-        vec_resize(&s->stack,vec_size(&s->stack)-1);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
         assert(reasons[v] != 0);
         c    = reasons[v];
 
@@ -544,15 +557,15 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
             int v = lit_var(clause_read_lit(c));
             if (tags[v] == l_Undef && levels[v] != 0){
                 if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-                    vec_push(&s->stack,(void*)v);
+                    veci_push(&s->stack,v);
                     tags[v] = l_True;
-                    vec_push(&s->tagged,(void*)v);
+                    veci_push(&s->tagged,v);
                 }else{
-                    int* tagged = (int*)vec_begin(&s->tagged);
+                    int* tagged = veci_begin(&s->tagged);
                     int j;
-                    for (j = top; j < vec_size(&s->tagged); j++)
+                    for (j = top; j < veci_size(&s->tagged); j++)
                         tags[tagged[j]] = l_Undef;
-                    vec_resize(&s->tagged,top);
+                    veci_resize(&s->tagged,top);
                     return 0;
                 }
             }
@@ -565,14 +578,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
                 if (tags[v] == l_Undef && levels[v] != 0){
                     if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
 
-                        vec_push(&s->stack,(void*)lit_var(lits[i]));
+                        veci_push(&s->stack,lit_var(lits[i]));
                         tags[v] = l_True;
-                        vec_push(&s->tagged,(void*)v);
+                        veci_push(&s->tagged,v);
                     }else{
-                        int* tagged = (int*)vec_begin(&s->tagged);
-                        for (j = top; j < vec_size(&s->tagged); j++)
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
                             tags[tagged[j]] = l_Undef;
-                        vec_resize(&s->tagged,top);
+                        veci_resize(&s->tagged,top);
                         return 0;
                     }
                 }
@@ -583,7 +596,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
     return 1;
 }
 
-static void solver_analyze(solver* s, clause* c, vec* learnt)
+static void solver_analyze(solver* s, clause* c, veci* learnt)
 {
     lit*     trail   = s->trail;
     lbool*   tags    = s->tags;
@@ -596,7 +609,7 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
     int      i, j, minl;
     int*     tagged;
 
-    vec_push(learnt,(void*)lit_Undef);
+    veci_push(learnt,lit_Undef);
 
     do{
         assert(c != 0);
@@ -606,12 +619,12 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
             assert(lit_var(q) >= 0 && lit_var(q) < s->size);
             if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
                 tags[lit_var(q)] = l_True;
-                vec_push(&s->tagged,(void*)lit_var(q));
+                veci_push(&s->tagged,lit_var(q));
                 act_var_bump(s,lit_var(q));
                 if (levels[lit_var(q)] == solver_dlevel(s))
                     cnt++;
                 else
-                    vec_push(learnt,(void*)q);
+                    veci_push(learnt,q);
             }
         }else{
 
@@ -625,12 +638,12 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
                 assert(lit_var(q) >= 0 && lit_var(q) < s->size);
                 if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
                     tags[lit_var(q)] = l_True;
-                    vec_push(&s->tagged,(void*)lit_var(q));
+                    veci_push(&s->tagged,lit_var(q));
                     act_var_bump(s,lit_var(q));
                     if (levels[lit_var(q)] == solver_dlevel(s))
                         cnt++;
                     else
-                        vec_push(learnt,(void*)q);
+                        veci_push(learnt,q);
                 }
             }
         }
@@ -643,31 +656,34 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
 
     }while (cnt > 0);
 
-    *(lit*)vec_begin(learnt) = neg(p);
+//    *veci_begin(learnt) = neg(p);
+
+    lits = veci_begin(learnt);
+    lits[0] = neg(p);
 
-    lits = (lit*)vec_begin(learnt);
     minl = 0;
-    for (i = 1; i < vec_size(learnt); i++){
+    for (i = 1; i < veci_size(learnt); i++){
         int lev = levels[lit_var(lits[i])];
         minl    |= 1 << (lev & 31);
     }
 
     // simplify (full)
-    for (i = j = 1; i < vec_size(learnt); i++){
+    for (i = j = 1; i < veci_size(learnt); i++){
         if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl))
             lits[j++] = lits[i];
     }
+//    j = veci_size(learnt);
 
     // update size of learnt + statistics
-    s->solver_stats.max_literals += vec_size(learnt);
-    vec_resize(learnt,j);
+    s->solver_stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
     s->solver_stats.tot_literals += j;
 
     // clear tags
-    tagged = (int*)vec_begin(&s->tagged);
-    for (i = 0; i < vec_size(&s->tagged); i++)
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
         tags[tagged[i]] = l_Undef;
-    vec_resize(&s->tagged,0);
+    veci_resize(&s->tagged,0);
 
 #ifdef DEBUG
     for (i = 0; i < s->size; i++)
@@ -676,14 +692,14 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
 
 #ifdef VERBOSEDEBUG
     printf(L_IND"Learnt {", L_ind);
-    for (i = 0; i < vec_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
 #endif
-    if (vec_size(learnt) > 1){
+    if (veci_size(learnt) > 1){
         int max_i = 1;
         int max   = levels[lit_var(lits[1])];
         lit tmp;
 
-        for (i = 2; i < vec_size(learnt); i++)
+        for (i = 2; i < veci_size(learnt); i++)
             if (levels[lit_var(lits[i])] > max){
                 max   = levels[lit_var(lits[i])];
                 max_i = i;
@@ -695,7 +711,7 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
     }
 #ifdef VERBOSEDEBUG
     {
-        int lev = vec_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
         printf(" } at level %d\n", lev);
     }
 #endif
@@ -824,15 +840,15 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
     double  random_var_freq = 0.0;//0.02;
 
     int     conflictC       = 0;
-    vec     learnt_clause;
+    veci    learnt_clause;
 
     assert(s->root_level == solver_dlevel(s));
 
     s->solver_stats.starts++;
     s->var_decay = (float)(1 / var_decay   );
     s->cla_decay = (float)(1 / clause_decay);
-    vec_resize(&s->model,0);
-    vec_new(&learnt_clause);
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
 
     for (;;){
         clause* confl = solver_propagate(s);
@@ -845,13 +861,13 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 #endif
             s->solver_stats.conflicts++; conflictC++;
             if (solver_dlevel(s) == s->root_level){
-                vec_delete(&learnt_clause);
+                veci_delete(&learnt_clause);
                 return l_False;
             }
 
-            vec_resize(&learnt_clause,0);
+            veci_resize(&learnt_clause,0);
             solver_analyze(s, confl, &learnt_clause);
-            blevel = vec_size(&learnt_clause) > 1 ? levels[lit_var(((lit*)vec_begin(&learnt_clause))[1])] : s->root_level;
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
             solver_canceluntil(s,blevel);
             solver_record(s,&learnt_clause);
             act_var_decay(s);
@@ -866,17 +882,17 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
                 // Reached bound on number of conflicts:
                 s->progress_estimate = solver_progress(s);
                 solver_canceluntil(s,s->root_level);
-                vec_delete(&learnt_clause);
+                veci_delete(&learnt_clause);
                 return l_Undef; 
             }
 
-            if ( s->nConfLimit && s->solver_stats.conflicts    > s->nConfLimit ||
-                 s->nImpLimit  && s->solver_stats.propagations > s->nImpLimit )
+            if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit ||
+                 s->nInsLimit  && s->solver_stats.inspects  > s->nInsLimit )
             {
                 // Reached bound on number of conflicts:
                 s->progress_estimate = solver_progress(s);
                 solver_canceluntil(s,s->root_level);
-                vec_delete(&learnt_clause);
+                veci_delete(&learnt_clause);
                 return l_Undef; 
             }
 
@@ -899,9 +915,9 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
                 // Model found:
                 lbool* values = s->assigns;
                 int i;
-                for (i = 0; i < s->size; i++) vec_push(&s->model,(void*)((int)values[i]));
+                for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
                 solver_canceluntil(s,s->root_level);
-                vec_delete(&learnt_clause);
+                veci_delete(&learnt_clause);
                 return l_True;
             }
 
@@ -922,11 +938,11 @@ solver* solver_new(void)
     // initialize vectors
     vec_new(&s->clauses);
     vec_new(&s->learnts);
-    vec_new(&s->order);
-    vec_new(&s->trail_lim);
-    vec_new(&s->tagged);
-    vec_new(&s->stack);
-    vec_new(&s->model);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
 
     // initialize arrays
     s->wlists    = 0;
@@ -975,6 +991,8 @@ solver* solver_new(void)
     s->pMem = Asat_MmStepStart( 10 );
 #endif
     s->pJMan = NULL;
+    s->pPrefVars = NULL;
+    s->nPrefVars = 0;
     s->timeTotal = clock();
     s->timeSelect = 0;
     s->timeUpdate = 0;
@@ -998,11 +1016,11 @@ void solver_delete(solver* s)
     // delete vectors
     vec_delete(&s->clauses);
     vec_delete(&s->learnts);
-    vec_delete(&s->order);
-    vec_delete(&s->trail_lim);
-    vec_delete(&s->tagged);
-    vec_delete(&s->stack);
-    vec_delete(&s->model);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
     free(s->binary);
 
     // delete arrays
@@ -1022,7 +1040,8 @@ void solver_delete(solver* s)
         free(s->tags     );
     }
 
-    if ( s->pJMan ) Asat_JManStop( s );
+    if ( s->pJMan )     Asat_JManStop( s );
+    if ( s->pPrefVars ) free( s->pPrefVars );
     free(s);
 }
 
@@ -1117,9 +1136,10 @@ bool   solver_simplify(solver* s)
 }
 
 
-bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit )
+bool solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit )
 {
     double  nof_conflicts = 100;
+//    double  nof_conflicts = 1000000;
     double  nof_learnts   = solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
@@ -1127,7 +1147,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit
 
     // set the external limits
     s->nConfLimit = nConfLimit;    // external limit on the number of conflicts
-    s->nImpLimit  = nImpLimit;     // external limit on the number of implications
+    s->nInsLimit  = nInsLimit;     // external limit on the number of implications
   
 
     for (i = begin; i < end; i++)
@@ -1160,6 +1180,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit
                 s->progress_estimate*100);
             fflush(stdout);
         }
+        s->nPrefDecNum = 0;
         status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
@@ -1170,9 +1191,9 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit
 //            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
         }
-        if ( s->nImpLimit  && s->solver_stats.propagations > s->nImpLimit )
+        if ( s->nInsLimit  && s->solver_stats.inspects > s->nInsLimit )
         {
-//            printf( "Reached the limit on the number of implications (%d).\n", s->nImpLimit );
+//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
         }
     }
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 3684d259..05e9dafa 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -37,9 +37,11 @@ extern "C" {
 // Simple types:
 
 //typedef int  bool;
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef int                lit;
 typedef char               lbool;
@@ -74,17 +76,19 @@ extern void    solver_delete(solver* s);
 
 extern bool    solver_addclause(solver* s, lit* begin, lit* end);
 extern bool    solver_simplify(solver* s);
-extern int     solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit );
+extern int     solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit );
 extern int *   solver_get_model( solver * p, int * pVars, int nVars );
 
 extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);
 
+
 // additional procedures
 extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        lit* assumptionsBegin, lit* assumptionsEnd,
                                        int incrementVars);
 extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
+extern void    Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars );
 
 // J-frontier support
 extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
@@ -131,12 +135,12 @@ struct solver_t
 
     clause*  binary;        // A temporary binary clause
     lbool*   tags;          //
-    vec      tagged;        // (contains: var)
-    vec      stack;         // (contains: var)
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
 
-    vec      order;         // Variable order. (heap) (contains: var)
-    vec      trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
-    vec      model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
 
     int      root_level;    // Level of first proper decision.
     int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
@@ -145,8 +149,8 @@ struct solver_t
     double   progress_estimate;
     int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
 
-    int      nConfLimit;    // external limit on the number of conflicts
-    int      nImpLimit;     // external limit on the number of implications
+    sint64   nConfLimit;    // external limit on the number of conflicts
+    sint64   nInsLimit;     // external limit on the number of implications
 
     // the memory manager
     Asat_MmStep_t *     pMem;
@@ -154,6 +158,12 @@ struct solver_t
     // J-frontier
     Asat_JMan_t *       pJMan;
 
+    // for making decisions on some variables first
+    int      nPrefDecNum;
+    int *    pPrefVars;
+    int      nPrefVars;
+
+    // solver statistics
     stats    solver_stats;
     int      timeTotal;
     int      timeSelect;
diff --git a/src/sat/asat/solver_vec.h b/src/sat/asat/solver_vec.h
index fae313d0..1ae30b0a 100644
--- a/src/sat/asat/solver_vec.h
+++ b/src/sat/asat/solver_vec.h
@@ -24,6 +24,35 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include <stdlib.h>
 
+// vector of 32-bit intergers (added for 64-bit portability)
+struct veci_t {
+    int    size;
+    int    cap;
+    int*   ptr;
+};
+typedef struct veci_t veci;
+
+static inline void veci_new (veci* v) {
+    v->size = 0;
+    v->cap  = 4;
+    v->ptr  = (int*)malloc(sizeof(int)*v->cap);
+}
+
+static inline void   veci_delete (veci* v)          { free(v->ptr);   }
+static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
+static inline int    veci_size   (veci* v)          { return v->size; }
+static inline void   veci_resize (veci* v, int k)   { v->size = k;    } // only safe to shrink !!
+static inline void   veci_push   (veci* v, int e)
+{
+    if (v->size == v->cap) {
+        int newsize = v->cap * 2+1;
+        v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+        v->cap = newsize; }
+    v->ptr[v->size++] = e;
+}
+
+
+// vector of 32- or 64-bit pointers
 struct vec_t {
     int    size;
     int    cap;
@@ -50,4 +79,5 @@ static inline void   vec_push   (vec* v, void* e)
     v->ptr[v->size++] = e;
 }
 
+
 #endif
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 9184cab9..353f6c4c 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -39,8 +39,7 @@ struct ABC_ManagerStruct_t
     Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
     // solving parameters
     int                   mode;          // 0 = resource-aware integration; 1 = brute-force SAT
-    int                   nConfLimit;    // time limit for pure SAT solving
-    int                   nImpLimit;     // time limit for pure SAT solving
+    Prove_Params_t        Params;        // integrated CEC parameters
     // information about the target 
     int                   nog;           // the numbers of gates in the target
     Vec_Ptr_t *           vNodes;        // the gates in the target
@@ -87,9 +86,11 @@ ABC_Manager ABC_InitManager()
     mng->pMmNames   = Extra_MmFlexStart();
     mng->vNodes     = Vec_PtrAlloc( 100 );
     mng->vValues    = Vec_IntAlloc( 100 );
-    mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT;
-    mng->nImpLimit  = ABC_DEFAULT_IMP_LIMIT;
     mng->mode       = 0; // set "resource-aware integration" as the default mode
+    // set default parameters for CEC
+    Prove_ParamsSetDefault( &mng->Params );
+    // set infinite resource limit for the final mitering
+    mng->Params.nMiteringLimitLast = ABC_INFINITY;
     return mng;
 }
 
@@ -334,7 +335,7 @@ int ABC_Check_Integrity( ABC_Manager mng )
             continue;
         if ( Abc_ObjFanoutNum(pObj) == 0 )
         {
-            printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
+//            printf( "ABC_Check_Integrity: The network has dangling nodes.\n" );
             return 0;
         }
     }
@@ -361,7 +362,7 @@ int ABC_Check_Integrity( ABC_Manager mng )
 ***********************************************************************/
 void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
 {
-    printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
+//    printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -377,7 +378,7 @@ void ABC_SetTimeLimit( ABC_Manager mng, int runtime )
 ***********************************************************************/
 void ABC_SetLearnLimit( ABC_Manager mng, int num )
 {
-    printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
+//    printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -393,7 +394,7 @@ void ABC_SetLearnLimit( ABC_Manager mng, int num )
 ***********************************************************************/
 void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
 {
-    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
+//    printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" );
 }
 
 /**Function*************************************************************
@@ -409,7 +410,7 @@ void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num )
 ***********************************************************************/
 void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
 {
-    mng->nConfLimit = num;
+    mng->Params.nMiteringLimitLast = num;
 }
 
 /**Function*************************************************************
@@ -425,7 +426,70 @@ void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num )
 ***********************************************************************/
 void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num )
 {
-    mng->nImpLimit = num;
+//    printf( "ABC_SetSolveImplicationLimit: The resource limit is not implemented (warning).\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num )
+{
+    mng->Params.nTotalBacktrackLimit = num;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num )
+{
+    mng->Params.nTotalInspectLimit = num;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+uint64 ABC_GetTotalBacktracksMade( ABC_Manager mng )
+{
+    return mng->Params.nTotalBacktracksMade;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+uint64 ABC_GetTotalInspectsMade( ABC_Manager mng )
+{
+    return mng->Params.nTotalInspectsMade;
 }
 
 /**Function*************************************************************
@@ -539,7 +603,7 @@ void ABC_AnalyzeTargets( ABC_Manager mng )
 ***********************************************************************/
 enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 {
-    Prove_Params_t Params, * pParams = &Params;
+    Prove_Params_t * pParams = &mng->Params;
     int RetValue, i;
 
     // check if the target network is available
@@ -548,16 +612,9 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 
     // try to prove the miter using a number of techniques
     if ( mng->mode )
-        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0, 0 );
+        RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
     else
-    {
-        // set default parameters for CEC
-        Prove_ParamsSetDefault( pParams );
-        // set infinite resource limit for the final mitering
-        pParams->nMiteringLimitLast = ABC_INFINITY;
-        // call the checker
         RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams );
-    }
 
     // analyze the result
     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index d2fa770e..b80eddbf 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -182,6 +182,11 @@ extern void                  ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num
 extern void                  ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
 extern void                  ABC_EnableDump(ABC_Manager mng, char* dump_file);
 
+extern void                  ABC_SetTotalBacktrackLimit( ABC_Manager mng, uint64 num );
+extern void                  ABC_SetTotalInspectLimit( ABC_Manager mng, uint64 num );
+extern uint64                ABC_GetTotalBacktracksMade( ABC_Manager mng );
+extern uint64                ABC_GetTotalInspectsMade( ABC_Manager mng );
+
 // the meaning of the parameters are:
 // nog: number of gates that are in the targets
 // names: name array of gates
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index d6215465..84363efe 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -27,6 +27,8 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#include "solver.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -49,8 +51,6 @@ struct Fraig_ParamsStruct_t_
     int  nPatsDyna;     // the number of words of dynamic simulation info
     int  nBTLimit;      // the max number of backtracks to perform
     int  nSeconds;      // the timeout for the final proof
-    int  nConfLimit;
-    int  nImpLimit;
     int  fFuncRed;      // performs only one level hashing
     int  fFeedBack;     // enables solver feedback
     int  fDist1Pats;    // enables distance-1 patterns
@@ -60,31 +60,39 @@ struct Fraig_ParamsStruct_t_
     int  fVerbose;      // the verbosiness flag
     int  fVerboseP;     // the verbosiness flag (for proof reporting)
     int  fInternal;     // is set to 1 for internal fraig calls
+    int  nConfLimit;    // the limit on the number of conflicts
+    sint64 nInspLimit;  // the limit on the number of inspections
 };
 
 struct Prove_ParamsStruct_t_
 {
     // general parameters
-    int   fUseFraiging;          // enables fraiging
-    int   fUseRewriting;         // enables rewriting
-    int   fUseBdds;              // enables BDD construction when other methods fail
-    int   fVerbose;              // prints verbose stats
+    int     fUseFraiging;          // enables fraiging
+    int     fUseRewriting;         // enables rewriting
+    int     fUseBdds;              // enables BDD construction when other methods fail
+    int     fVerbose;              // prints verbose stats
     // iterations
-    int   nItersMax;             // the number of iterations
+    int     nItersMax;             // the number of iterations
     // mitering 
-    int   nMiteringLimitStart;   // starting mitering limit
-    float nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    int     nMiteringLimitStart;   // starting mitering limit
+    float   nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
     // rewriting 
-    int   nRewritingLimitStart;  // the number of rewriting iterations
-    float nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
+    int     nRewritingLimitStart;  // the number of rewriting iterations
+    float   nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
     // fraiging 
-    int   nFraigingLimitStart;   // starting backtrack(conflict) limit
-    float nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    int     nFraigingLimitStart;   // starting backtrack(conflict) limit
+    float   nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
     // last-gasp BDD construction
-    int   nBddSizeLimit;         // the number of BDD nodes when construction is aborted
-    int   fBddReorder;           // enables dynamic BDD variable reordering
+    int     nBddSizeLimit;         // the number of BDD nodes when construction is aborted
+    int     fBddReorder;           // enables dynamic BDD variable reordering
     // last-gasp mitering
-    int   nMiteringLimitLast;    // final mitering limit
+    int     nMiteringLimitLast;    // final mitering limit
+    // global SAT solver limits
+    sint64  nTotalBacktrackLimit;  // global limit on the number of backtracks
+    sint64  nTotalInspectLimit;    // global limit on the number of clause inspects
+    // global resources applied
+    sint64  nTotalBacktracksMade;  // the total number of backtracks made
+    sint64  nTotalInspectsMade;    // the total number of inspects made
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -137,6 +145,8 @@ extern int                 Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
 extern int                 Fraig_ManReadSatFails( Fraig_Man_t * p );      
+extern int                 Fraig_ManReadConflicts( Fraig_Man_t * p );      
+extern int                 Fraig_ManReadInspects( Fraig_Man_t * p );      
 
 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index b4bdbcab..79a7c224 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -66,6 +66,10 @@ int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           {
 int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }
 // returns the number of times FRAIG package timed out
 int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFailsReal;    }      
+// returns the number of conflicts in the SAT solver
+int               Fraig_ManReadConflicts( Fraig_Man_t * p )                   { return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; }      
+// returns the number of inspections in the SAT solver
+int               Fraig_ManReadInspects( Fraig_Man_t * p )                    { return p->pSat? Msat_SolverReadInspects(p->pSat) : 0;   }            
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 4ebb9a9f..89bc924f 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -49,6 +49,7 @@
 Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 )
 {
     Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
+    int fUseSatCheck;
 //    int RetValue;
 
     // check for trivial cases
@@ -167,7 +168,8 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
     // there is another node which looks the same according to simulation
 
     // use SAT to resolve the ambiguity
-    if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
+    fUseSatCheck = (pMan->nInspLimit == 0 || Fraig_ManReadInspects(pMan) < pMan->nInspLimit); 
+    if ( fUseSatCheck && Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) )
     {
         // set the node to be equivalent with this node
         // to prevent loops, only set if the old node is not in the TFI of the new node
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 8e016331..9c6e0d47 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -66,7 +66,7 @@
 // the bit masks
 #define FRAIG_MASK(n)             ((~((unsigned)0)) >> (32-(n)))
 #define FRAIG_FULL                 (~((unsigned)0))
-#define FRAIG_NUM_WORDS(n)         ((n)/32 + (((n)%32) > 0))
+#define FRAIG_NUM_WORDS(n)         (((n)>>5) + (((n)&31) > 0))
 
 // maximum/minimum operators
 #define FRAIG_MIN(a,b)             (((a) < (b))? (a) : (b))
@@ -152,6 +152,7 @@ struct Fraig_ManStruct_t_
     int                   fTryProve;     // tries to solve the final miter
     int                   fVerbose;      // the verbosiness flag
     int                   fVerboseP;     // the verbosiness flag
+    sint64                nInspLimit;    // the inspection limit
 
     int                   nTravIds;      // the traversal counter
     int                   nTravIds2;     // the traversal counter
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 3268ac3a..ffb51a07 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -42,10 +42,12 @@ int timeAssign;
 ***********************************************************************/
 void Prove_ParamsSetDefault( Prove_Params_t * pParams )
 {
+    // clean the parameter structure
+    memset( pParams, 0, sizeof(Prove_Params_t) );
     // general parameters
     pParams->fUseFraiging         = 1;       // enables fraiging
     pParams->fUseRewriting        = 1;       // enables rewriting
-    pParams->fUseBdds             = 1;       // enables BDD construction when other methods fail
+    pParams->fUseBdds             = 0;       // enables BDD construction when other methods fail
     pParams->fVerbose             = 0;       // prints verbose stats
     // iterations
     pParams->nItersMax            = 6;       // the number of iterations
@@ -63,6 +65,9 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
     pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
     // last-gasp mitering
     pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+    // global SAT solver limits
+    pParams->nTotalBacktrackLimit = 0;       // global limit on the number of backtracks
+    pParams->nTotalInspectLimit   = 0;       // global limit on the number of clause inspects
 }
 
 /**Function*************************************************************
@@ -92,6 +97,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
     pParams->fVerbose   =  0;                     // the verbosiness flag
     pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
     pParams->fInternal  =  0;                     // the flag indicates the internal run 
+    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
+    pParams->nInspLimit =  0;                     // the limit on the number of inspections
 }
 
 /**Function*************************************************************
@@ -121,6 +128,8 @@ void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
     pParams->fVerbose   =  0;                     // the verbosiness flag
     pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
     pParams->fInternal  =  0;                     // the flag indicates the internal run 
+    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
+    pParams->nInspLimit =  0;                     // the limit on the number of inspections
 }
 
 /**Function*************************************************************
@@ -176,6 +185,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     p->fTryProve  = pParams->fTryProve;   // disable accumulation of structural choices (keeps only the first choice)
     p->fVerbose   = pParams->fVerbose;    // disable verbose output
     p->fVerboseP  = pParams->fVerboseP;   // disable verbose output
+    p->nInspLimit = pParams->nInspLimit;  // the limit on the number of inspections
 
     // start memory managers
     p->mmNodes    = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 94416a5d..5f8603a7 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -97,6 +97,7 @@ extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
 extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
 extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
 extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
+extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
 extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
 extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
 extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 3dfe2109..03e7b873 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -56,10 +56,10 @@ typedef long long   int64;
 #define ALLOC(type, num)    \
     ((type *) malloc(sizeof(type) * (num)))
 #define REALLOC(type, obj, num)    \
-    (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
+    ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num))))
 #define FREE(obj)        \
-    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+    ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
 
 // By default, custom memory management is used
 // which guarantees constant time allocation/deallocation 
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 4a721487..e3d85774 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -41,26 +41,27 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
   SeeAlso     []
 
 ***********************************************************************/
-int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;     }
-int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;     }
-int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc;}
+int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;      }
+int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;   }
+int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc; }
 int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
-int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;    }
-Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )             { return p->pReasons;  }
+int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;     }
+Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )            { return p->pReasons;   }
 Msat_Lit_t          Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
-Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                 { return p->vLearned;  }
-Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )            { return p->pvWatched; }
-int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;  }
-int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;  }
-int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return p->nBackTracks; }
-Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                     { return p->pMem;      }
-int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;     }
-int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId; }
+Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                { return p->vLearned;   }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )           { return p->pvWatched;  }
+int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;   }
+int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;     }
+int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return (int)p->Stats.nConflicts; }
+int                Msat_SolverReadInspects( Msat_Solver_t * p )                { return (int)p->Stats.nInspects;  }
+Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                    { return p->pMem;       }
+int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;      }
+int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId;  }
 void               Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose )  { p->fVerbose = fVerbose; }
-void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;  }
-void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;  }
-void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++; }
-void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--; }
+void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;   }
+void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;   }
+void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++;  }
+void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--;  }
 void               Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p )         { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
 void               Msat_SolverMarkClausesStart( Msat_Solver_t * p )            { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }