Version abc80130

16 files changed, 65 insertions, 135 deletions

diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 53353ba6..21ddcb81 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,10 +21,6 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -69,7 +65,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
@@ -80,10 +76,10 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
 /*=== satSolver.c ===========================================================*/
 // adding vars, clauses, simplifying the database, and solving
-extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
+extern bool             Msat_SolverAddVar( Msat_Solver_t * p );
 extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
 extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
+extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit );
 // printing stats, assignments, and clauses
 extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
 extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
@@ -91,20 +87,17 @@ extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
 extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
 // access to the solver internal data
 extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
-extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
 extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
 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 );
 extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
 extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
 extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
-extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
 // returns the solution after incremental solving
 extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
 extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
@@ -160,13 +153,8 @@ extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
 extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
- 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index 1cd795bd..c9a518ce 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -45,9 +45,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
     if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
         return;
     Var = MSAT_LIT2VAR(Lit);
-    p->pdActivity[Var] += p->dVarInc;
-//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
-    if ( p->pdActivity[Var] > 1e100 )
+    if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index 2ba8cd32..dc39bee6 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -36,7 +36,7 @@ struct Msat_Clause_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -82,10 +82,6 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         // nSeenId - 1 stands for negative
         // nSeenId     stands for positive
         // Remove false literals
-
-        // there is a bug here!!!!
-        // when the same var in opposite polarities is given, it drops one polarity!!!
-
         for ( i = j = 0; i < nLits; i++ ) {
             // get the corresponding variable
             Var  = MSAT_LIT2VAR(pLits[i]);
@@ -194,7 +190,6 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         {
             Msat_SolverVarBumpActivity( p, pLits[i] );
 //            Msat_SolverVarBumpActivity( p, pLits[i] );
-//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
         }
     }
 
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
index 04691cf2..7c24619f 100644
--- a/src/sat/msat/msatClauseVec.c
+++ b/src/sat/msat/msatClauseVec.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 03903abe..037616f6 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 
@@ -119,7 +119,6 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
-    float *             pFactors;    // the multiplicative factors of variable activity
     double              dVarInc;     // Amount to bump next variable with.
     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
@@ -152,7 +151,6 @@ struct Msat_Solver_t_
     int                 nSeenId;     // the id of current seeing
     Msat_IntVec_t *     vReason;     // the temporary array of literals
     Msat_IntVec_t *     vTemp;       // the temporary array of literals
-    int *               pFreq;       // the number of times each var participated in conflicts
 
     // the memory manager
     Msat_MmStep_t *     pMem;
@@ -186,7 +184,7 @@ struct Msat_IntVec_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 30bf4a96..2d178094 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -72,7 +72,7 @@ struct Msat_MmStep_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
     int i;
     char * pTemp;
 
-    // deallocate all chunks except the first one
+    // delocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 956e7fc6..ca034233 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -58,7 +58,7 @@ static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
 extern int timeSelect;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index 4db7ff7b..6067b40f 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -38,7 +38,7 @@ struct Msat_OrderVar_t_
 {
     Msat_OrderVar_t    * pNext;
     Msat_OrderVar_t    * pPrev;
-    int                  Num;
+    int                 Num;
 };
 
 // the ring of variables data structure (J-boundary)
@@ -82,7 +82,7 @@ extern int timeSelect;
 extern int timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -170,8 +170,7 @@ int Msat_OrderCheck( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext;
     Msat_IntVec_t * vRound;
     int * pRound, nRound;
-    int * pVars, nVars, i, k;
-    int Counter = 0;
+    int * pVars, nVars, i;
 
     // go through all the variables in the boundary
     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
@@ -189,14 +188,10 @@ int Msat_OrderCheck( Msat_Order_t * p )
             if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                 break;
         }
-//        assert( i != nRound );
-//        if ( i == nRound )
-//            return 0;
-        if ( i == nRound )
-            Counter++;
+        assert( i != nRound );
+        if ( i != nRound )
+            return 0;
     }
-    if ( Counter > 0 )
-        printf( "%d(%d) ", Counter, p->rVars.nItems );
 
     // we may also check other unassigned variables in the cone
     // to make sure that if they are not in J-boundary, 
@@ -214,16 +209,16 @@ int Msat_OrderCheck( Msat_Order_t * p )
         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
         nRound = Msat_IntVecReadSize( vRound );
         pRound = Msat_IntVecReadArray( vRound );
-        for ( k = 0; k < nRound; k++ )
+        for ( i = 0; i < nRound; i++ )
         {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
                 continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
+            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                 break;
         }
-//        assert( k == nRound );
-//        if ( k != nRound )
-//            return 0;
+        assert( i == nRound );
+        if ( i == nRound )
+            return 0;
     }
     return 1;
 }
@@ -261,7 +256,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
     double * pdActs = p->pSat->pdActivity;
     double dfActBest;
-//    int clk = clock();
+    int clk = clock();
 
     pVarBest = NULL;
     dfActBest = -1.0;
@@ -273,13 +268,12 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
             pVarBest  = pVar;
         }
     }
-//timeSelect += clock() - clk;
-//timeAssign += clock() - clk;
+timeSelect += clock() - clk;
+timeAssign += clock() - clk;
 
 //if ( pVarBest && pVarBest->Num % 1000 == 0 )
 //printf( "%d ", p->rVars.nItems );
 
-//    Msat_OrderCheck( p );
     if ( pVarBest )
     {
         assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
@@ -302,7 +296,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
 void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound;
-    int i;//, clk = clock();
+    int i, clk = clock();
 
     // make sure the variable is in the boundary
     assert( Var < p->nVarsAlloc );
@@ -322,7 +316,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
             continue;
         Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
     }
-//timeSelect += clock() - clk;
+timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -340,7 +334,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
 void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound, * vRound2;
-    int i, k;//, clk = clock();
+    int i, k, clk = clock();
 
     // make sure the variable is not in the boundary
     assert( Var < p->nVarsAlloc );
@@ -369,7 +363,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
             if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
                 Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
         }
-//timeSelect += clock() - clk;
+timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -456,7 +450,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
         pRing->pRoot = pVar->pNext;
     // move the root to the next entry after pVar
     // this way all the additions to the list will be traversed first
-//    pRing->pRoot = pVar->pPrev;
+//    pRing->pRoot = pVar->pNext;
     // delete the node
     pVar->pPrev->pNext = pVar->pNext;
     pVar->pNext->pPrev = pVar->pPrev;
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
index 5938e042..c12cc75d 100644
--- a/src/sat/msat/msatQueue.c
+++ b/src/sat/msat/msatQueue.c
@@ -33,7 +33,7 @@ struct Msat_Queue_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index 738562ef..b8e585a4 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -27,7 +27,7 @@
 static char * Msat_FileRead( FILE * pFile );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index ee3507a6..ba506993 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -27,7 +27,7 @@
 static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -41,30 +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_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 (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;  }
+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; }
 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); }
-float *            Msat_SolverReadFactors( Msat_Solver_t * p )                 { return p->pFactors;   }
 
 /**Function*************************************************************
 
@@ -175,12 +172,8 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pFactors   = ALLOC( float, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
-    {
-        p->pdActivity[i] = 0.0;
-        p->pFactors[i]   = 1.0;
-    }
+        p->pdActivity[i] = 0;
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
     p->pModel    = ALLOC( int, p->nVarsAlloc ); 
@@ -244,12 +237,8 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-    {
-        p->pdActivity[i] = 0.0;
-        p->pFactors[i]   = 1.0;
-    }
+        p->pdActivity[i] = 0;
 
     p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
     p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
@@ -403,7 +392,6 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
-    FREE( p->pFactors );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index f9fee73c..b8d9f328 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -39,11 +39,10 @@
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
+bool Msat_SolverAddVar( Msat_Solver_t * p )
 {
     if ( p->nVars == p->nVarsAlloc )
         Msat_SolverResize( p, 2 * p->nVarsAlloc );
-    p->pLevel[p->nVars] = Level;
     p->nVars++;
     return 1;
 }
@@ -132,18 +131,14 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
+bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit )
 {
     Msat_SearchParams_t Params = { 0.95, 0.999 };
     double nConflictsLimit, nLearnedLimit;
     Msat_Type_t Status;
-    int timeStart = clock();
     int64 nConflictsOld = p->Stats.nConflicts;
     int64 nDecisionsOld = p->Stats.nDecisions;
 
-//    p->pFreq = ALLOC( int, p->nVarsAlloc );
-//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
- 
     if ( vAssumps )
     {
         int * pAssumps, nAssumps, i;
@@ -177,31 +172,11 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         nConflictsLimit *= 1.5;
         nLearnedLimit   *= 1.1;
         // if the limit on the number of backtracks is given, quit the restart loop
-        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
-            break;
-        // if the runtime limit is exceeded, quit the restart loop
-        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+        if ( nBackTrackLimit > 0 )
             break;
     }
     Msat_SolverCancelUntil( p, 0 );
     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
-/*
-    PRT( "True solver runtime", clock() - timeStart );
-    // print the statistics
-    {
-        int i, Counter = 0;
-        for ( i = 0; i < p->nVars; i++ )
-            if ( p->pFreq[i] > 0 )
-            {
-                printf( "%d ", p->pFreq[i] );
-                Counter++;
-            }
-        if ( Counter )
-            printf( "\n" );
-        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
-        PRT( "Time", clock() - timeStart );
-    }
-*/
     return Status;
 }
 
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
index 05b7f6a9..f17595a7 100644
--- a/src/sat/msat/msatSolverIo.c
+++ b/src/sat/msat/msatSolverIo.c
@@ -27,7 +27,7 @@
 static char * Msat_TimeStamp();
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 11a6540c..13a0c403 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -31,7 +31,7 @@ static void            Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC
 static void            Msat_SolverReduceDB( Msat_Solver_t * p );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -534,18 +534,12 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
     Msat_Clause_t * pConf;
     Msat_Var_t Var;
     int nLevelBack, nConfs, nAssigns, Value;
-    int i;
 
     assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
     p->Stats.nStarts++;
     p->dVarDecay = 1 / pPars->dVarDecay;
     p->dClaDecay = 1 / pPars->dClaDecay;
 
-    // reset the activities
-    for ( i = 0; i < p->nVars; i++ )
-       p->pdActivity[i] = (double)p->pFactors[i];
-//       p->pdActivity[i] = 0.0;
-
     nConfs = 0;
     while ( 1 )
     {
@@ -605,7 +599,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
                 return MSAT_UNKNOWN; 
             }
-            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
+            else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) {
                 // Reached bound on number of conflicts:
                 Msat_QueueClear( p->pQueue );
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
index 3b89d102..2198d303 100644
--- a/src/sat/msat/msatSort.c
+++ b/src/sat/msat/msatSort.c
@@ -41,7 +41,7 @@ static int irand(double seed, int size) {
 static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 75f53047..951969cf 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -28,7 +28,7 @@ static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
 static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************