7 files changed, 7 insertions, 11 deletions
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 79c0655b..ecad9d37 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -569,7 +569,7 @@ void ABC_SolveInit( ABC_Manager mng )
     if ( mng->nog == 0 )
         { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; }
 
-    // ABC_FREE the previous target network if present
+    // free the previous target network if present
     if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
 
     // set the new target network
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 7d99d146..7977824d 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -412,7 +412,7 @@ void Fraig_FeedBackCovering( Fraig_Man_t * p, Msat_IntVec_t * vPats )
         Msat_IntVecPush( vPats, iPat );
     }
 
-    // ABC_FREE the set of columns
+    // free the set of columns
     for ( i = 0; i < vColumns->nSize; i++ )
         Fraig_MemFixedEntryRecycle( p->mmSims, (char *)vColumns->pArray[i] );
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 3bea5e42..ac6ea873 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -68,10 +68,6 @@
 #define FRAIG_FULL                 (~((unsigned)0))
 #define FRAIG_NUM_WORDS(n)         (((n)>>5) + (((n)&31) > 0))
 
-// maximum/minimum operators
-#define FRAIG_MIN(a,b)             (((a) < (b))? (a) : (b))
-#define FRAIG_MAX(a,b)             (((a) > (b))? (a) : (b))
-
 // generating random unsigned (#define RAND_MAX 0x7fff)
 #define FRAIG_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
 
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 6e3d3c7d..4cfe035d 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -174,7 +174,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_
     pNode->NumPi = -1;
 
     // compute the level of this node
-    pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
+    pNode->Level = 1 + ABC_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
     pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
 
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 66698600..084d1538 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -1434,7 +1434,7 @@ void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
     float * pFactors = Msat_SolverReadFactors(pMan->pSat);
     if ( pFactors == NULL )
         return;
-    MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
+    MaxLevel = ABC_MAX( pOld->Level, pNew->Level );
     // create the variable order
     for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
     {
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index ea52d363..0930edbd 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -457,7 +457,7 @@ int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int
     // compute levels of the children nodes
     Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum );
     Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum );
-    pNode->Level = 1 + FRAIG_MAX( Level1, Level2 );
+    pNode->Level = 1 + ABC_MAX( Level1, Level2 );
     if ( pNode->pNextE )
     {
         LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index dece390c..6a518212 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -304,7 +304,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
 void Msat_SolverClean( Msat_Solver_t * p, int nVars )
 {
     int i;
-    // ABC_FREE the clauses
+    // free the clauses
     int nClauses;
     Msat_Clause_t ** pClauses;
 
@@ -384,7 +384,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
 {
     int i;
 
-    // ABC_FREE the clauses
+    // free the clauses
     int nClauses;
     Msat_Clause_t ** pClauses;
 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ),