diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
index 217d32692..6d6a2f226 100644
--- a/src/aig/saig/saigTrans.c
+++ b/src/aig/saig/saigTrans.c
@@ -6,7 +6,7 @@
 
   PackageName [Sequential AIG package.]
 
-  Synopsis    [Dynamic simplication of the transition relation.]
+  Synopsis    [Dynamic simplification of the transition relation.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h
index 37f007205..98e088e45 100644
--- a/src/proof/fraig/fraigInt.h
+++ b/src/proof/fraig/fraigInt.h
@@ -383,7 +383,7 @@ extern void                Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordSt
 /*=== fraigPrime.c =============================================================*/
 extern int                 s_FraigPrimes[FRAIG_MAX_PRIMES];
 /*=== fraigSat.c ===============================================================*/
-extern int                 Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
+extern int                 Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
 /*=== fraigTable.c =============================================================*/
 extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize );
 extern void                Fraig_HashTableFree( Fraig_HashTable_t * p );
diff --git a/src/proof/fraig/fraigSat.c b/src/proof/fraig/fraigSat.c
index 7cad3eab3..433cc4f99 100644
--- a/src/proof/fraig/fraigSat.c
+++ b/src/proof/fraig/fraigSat.c
@@ -548,7 +548,7 @@ p->time3 += Abc_Clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
+int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
 {
     int RetValue, RetValue1, i, fComp;
     abctime clk;
diff --git a/src/proof/fraig/fraigUtil.c b/src/proof/fraig/fraigUtil.c
index 7869c6d61..d5e8b59bf 100644
--- a/src/proof/fraig/fraigUtil.c
+++ b/src/proof/fraig/fraigUtil.c
@@ -872,13 +872,13 @@ clk = Abc_Clock();
             pNode2 = vPivots->pArray[k];
             if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
             {
-                if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
+                if ( Fraig_NodeIsImplification( pMan, pNode, pNode2, -1 ) )
                     nProved++;
                 Counter++;
             }
             else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
             {
-                if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
+                if ( Fraig_NodeIsImplification( pMan, pNode2, pNode, -1 ) )
                     nProved++;
                 Counter++;
             }
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 9c23e0d00..cbaedbe62 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -842,7 +842,7 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )
     if ( pPars->pre ) 
     {
         S.eliminate(true);
-        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
         if ( fDumpCnf )
@@ -1510,7 +1510,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
     if (pPars->pre) 
     {
         S.eliminate(true);
-        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
     
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index 99ca112ae..0e4871187 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -869,7 +869,7 @@ void Glucose2_SolveCnf( char * pFileName, Glucose2_Pars * pPars )
     if ( pPars->pre ) 
     {
         S.eliminate(true);
-        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
 
@@ -1528,7 +1528,7 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
     if (pPars->pre) 
     {
         S.eliminate(true);
-        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        printf( "c Simplification removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }