diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index e92e512c46..beb24e54a8 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -225,7 +225,7 @@ static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                            }
+static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1UL << (ObjId & 31));                            }
 static inline int          Aig_WordCountOnes( unsigned uWord )
 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index ee82b08417..d3a2ae41a2 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -175,10 +175,10 @@ static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
 #define KIT_MAX(a,b)       (((a) > (b))? (a) : (b))
 #define KIT_INFINITY       (100000000)
 
-static inline int          Kit_CubeHasLit( unsigned uCube, int i )                        { return(uCube &  (unsigned)(1<<i)) > 0;  }
-static inline unsigned     Kit_CubeSetLit( unsigned uCube, int i )                        { return uCube |  (unsigned)(1<<i);       }
-static inline unsigned     Kit_CubeXorLit( unsigned uCube, int i )                        { return uCube ^  (unsigned)(1<<i);       }
-static inline unsigned     Kit_CubeRemLit( unsigned uCube, int i )                        { return uCube & ~(unsigned)(1<<i);       }
+static inline int          Kit_CubeHasLit( unsigned uCube, int i )                        { return(uCube &  (unsigned)(1UL<<i)) > 0;  }
+static inline unsigned     Kit_CubeSetLit( unsigned uCube, int i )                        { return uCube |  (unsigned)(1UL<<i);       }
+static inline unsigned     Kit_CubeXorLit( unsigned uCube, int i )                        { return uCube ^  (unsigned)(1UL<<i);       }
+static inline unsigned     Kit_CubeRemLit( unsigned uCube, int i )                        { return uCube & ~(unsigned)(1UL<<i);       }
 
 static inline int          Kit_CubeContains( unsigned uLarge, unsigned uSmall )           { return (uLarge & uSmall) == uSmall;     }
 static inline unsigned     Kit_CubeSharp( unsigned uCube, unsigned uMask )                { return uCube & ~uMask;                  }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 2f3a84db74..9a7dffd051 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -515,9 +515,9 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
     for (i = 0; i < (int)c->size; i++)
     {
         lev = var_level(s, lit_var(c->lits[i]));
-        if ( !(minl & (1 << (lev & 31))) )
+        if ( !(minl & (1UL << (lev & 31))) )
         {
-            minl |= 1 << (lev & 31);
+            minl |= 1UL << (lev & 31);
             lbd++;
 //            printf( "%d ", lev );
         }
@@ -793,7 +793,7 @@ static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
             for (i = 1; i < clause_size(c); i++){
                 int v = lit_var(lits[i]);
                 if (!var_tag(s,v) && var_level(s, v)){
-                    if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
+                    if (s->reasons[v] != 0 && ((1UL << (var_level(s, v) & 31)) & minl)){
                         veci_push(&s->stack,lit_var(lits[i]));
                         var_set_tag(s, v, 1);
                     }else{
@@ -963,7 +963,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
     minl = 0;
     for (i = 1; i < veci_size(learnt); i++){
         int lev = var_level(s, lit_var(lits[i]));
-        minl    |= 1 << (lev & 31);
+        minl    |= 1UL << (lev & 31);
     }
 
     // simplify (full)