diff --git a/regression/smt2_solver/basic-bv1/basic-bv1.smt2 b/regression/smt2_solver/basic-bv1/basic-bv1.smt2
index 13c3a739dcb..c3a68cd30c0 100644
--- a/regression/smt2_solver/basic-bv1/basic-bv1.smt2
+++ b/regression/smt2_solver/basic-bv1/basic-bv1.smt2
@@ -14,6 +14,10 @@
 (define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right
 (define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a
 
+; rotation
+(define-fun b11 () Bool (= ((_ rotate_left 2) #xf7) #xdf)) ; rotation left
+(define-fun b12 () Bool (= ((_ rotate_right 2) #x07) #xc1)) ; rotation right
+
 ; Bitwise Operations
 
 (define-fun w1 () Bool (= (bvor #x6 #x3) #x7))   ; bitwise or
@@ -56,7 +60,7 @@
 ; all must be true
 
 (assert (not (and
-  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10
+  b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 b11 b12
   d01
   power-test
   p1 p2 p3 p4 p5 p6 p7 p8)))
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 4c4d5b60bd2..12571a7c01d 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -216,7 +216,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_div(to_div_expr(expr));
   else if(expr.id()==ID_mod)
     return convert_mod(to_mod_expr(expr));
-  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
+  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
+          expr.id()==ID_rol || expr.id()==ID_ror)
     return convert_shift(to_shift_expr(expr));
   else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
           expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index ceef7d19f0d..f7e4798f780 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -112,7 +112,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
 
     bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
 
-    bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::LEFT, bv1);
+    bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);
 
     // a negative shift is undefined; yet this isn't an overflow
     literalt neg_shift =
diff --git a/src/solvers/flattening/boolbv_power.cpp b/src/solvers/flattening/boolbv_power.cpp
index e9967a46860..c52f3ba7f17 100644
--- a/src/solvers/flattening/boolbv_power.cpp
+++ b/src/solvers/flattening/boolbv_power.cpp
@@ -29,7 +29,7 @@ bvt boolbvt::convert_power(const binary_exprt &expr)
       bv_utils.equal(op0, bv_utils.build_constant(2, op0.size()));
 
     bvt one=bv_utils.build_constant(1, width);
-    bvt shift=bv_utils.shift(one, bv_utilst::shiftt::LEFT, op1);
+    bvt shift=bv_utils.shift(one, bv_utilst::shiftt::SHIFT_LEFT, op1);
 
     bvt nondet=prop.new_variables(width);
 
diff --git a/src/solvers/flattening/boolbv_shift.cpp b/src/solvers/flattening/boolbv_shift.cpp
index 596d51067e2..be75dce3ef7 100644
--- a/src/solvers/flattening/boolbv_shift.cpp
+++ b/src/solvers/flattening/boolbv_shift.cpp
@@ -30,9 +30,6 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.operands().size()!=2)
-    throw "shifting takes two operands";
-
   const bvt &op=convert_bv(expr.op0());
 
   if(op.size()!=width)
@@ -41,11 +38,15 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   bv_utilst::shiftt shift;
 
   if(expr.id()==ID_shl)
-    shift=bv_utilst::shiftt::LEFT;
+    shift=bv_utilst::shiftt::SHIFT_LEFT;
   else if(expr.id()==ID_ashr)
-    shift=bv_utilst::shiftt::ARIGHT;
+    shift=bv_utilst::shiftt::SHIFT_ARIGHT;
   else if(expr.id()==ID_lshr)
-    shift=bv_utilst::shiftt::LRIGHT;
+    shift=bv_utilst::shiftt::SHIFT_LRIGHT;
+  else if(expr.id()==ID_rol)
+    shift=bv_utilst::shiftt::ROTATE_LEFT;
+  else if(expr.id()==ID_ror)
+    shift=bv_utilst::shiftt::ROTATE_RIGHT;
   else
     throw "unexpected shift operator";
 
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 1d729070c12..962336c1b29 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -482,26 +482,45 @@ bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
   bvt result;
   result.resize(src.size());
 
+  // 'dist' is user-controlled, and thus arbitary.
+  // We thus must guard against the case in which i+dist overflows.
+  // We do so by considering the case dist>=src.size().
+
   for(std::size_t i=0; i<src.size(); i++)
   {
     literalt l;
 
     switch(s)
     {
-    case shiftt::LEFT:
+    case shiftt::SHIFT_LEFT:
+      // no underflow on i-dist because of condition dist<=i
       l=(dist<=i?src[i-dist]:const_literal(false));
       break;
 
-    case shiftt::ARIGHT:
-      l=(i+dist<src.size()?src[i+dist]:src[src.size()-1]); // sign bit
+    case shiftt::SHIFT_ARIGHT:
+      // src.size()-i won't underflow as i<src.size()
+      // Then, if dist<src.size()-i, then i+dist<src.size()
+      l=(dist<src.size()-i?src[i+dist]:src[src.size()-1]); // sign bit
+      break;
+
+    case shiftt::SHIFT_LRIGHT:
+      // src.size()-i won't underflow as i<src.size()
+      // Then, if dist<src.size()-i, then i+dist<src.size()
+      l=(dist<src.size()-i?src[i+dist]:const_literal(false));
       break;
 
-    case shiftt::LRIGHT:
-      l=(i+dist<src.size()?src[i+dist]:const_literal(false));
+    case shiftt::ROTATE_LEFT:
+      // prevent overflows by using dist%src.size()
+      l=src[(src.size()+i-(dist%src.size()))%src.size()];
+      break;
+
+    case shiftt::ROTATE_RIGHT:
+      // prevent overflows by using dist%src.size()
+      l=src[(i+(dist%src.size()))%src.size()];
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
 
     result[i]=l;
diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h
index 0dc828a773d..c76ad8274ff 100644
--- a/src/solvers/flattening/bv_utils.h
+++ b/src/solvers/flattening/bv_utils.h
@@ -68,7 +68,11 @@ class bv_utilst
   literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep);
   literalt carry_out(const bvt &op0, const bvt &op1, literalt carry_in);
 
-  enum class shiftt { LEFT, LRIGHT, ARIGHT };
+  enum class shiftt
+  {
+    SHIFT_LEFT, SHIFT_LRIGHT, SHIFT_ARIGHT, ROTATE_LEFT, ROTATE_RIGHT
+  };
+
   bvt shift(const bvt &op, const shiftt shift, std::size_t distance);
   bvt shift(const bvt &op, const shiftt shift, const bvt &distance);
 
diff --git a/src/solvers/floatbv/float_approximation.cpp b/src/solvers/floatbv/float_approximation.cpp
index 2c73e517999..63d2e372813 100644
--- a/src/solvers/floatbv/float_approximation.cpp
+++ b/src/solvers/floatbv/float_approximation.cpp
@@ -42,7 +42,8 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent)
     if(over_approximate)
       shifted_fraction=overapproximating_left_shift(fraction, i);
     else
-      shifted_fraction=bv_utils.shift(fraction, bv_utilst::shiftt::LEFT, i);
+      shifted_fraction=bv_utils.shift(
+        fraction, bv_utilst::shiftt::SHIFT_LEFT, i);
 
     bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
 
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index 600add64d5e..cb2fce7c329 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -106,7 +106,7 @@ bvt float_utilst::to_integer(
                                        unpacked.exponent.size());
     bvt distance=bv_utils.sub(offset, unpacked.exponent);
     bvt shift_result=bv_utils.shift(
-      fraction, bv_utilst::shiftt::LRIGHT, distance);
+      fraction, bv_utilst::shiftt::SHIFT_LRIGHT, distance);
 
     // if the exponent is negative, we have zero anyways
     bvt result=shift_result;
@@ -809,7 +809,7 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
     // If so, shift the zeros out left by 'distance'.
     // Otherwise, leave as is.
     const bvt shifted=
-      bv_utils.shift(fraction, bv_utilst::shiftt::LEFT, distance);
+      bv_utils.shift(fraction, bv_utilst::shiftt::SHIFT_LEFT, distance);
 
     fraction=
       bv_utils.select(prefix_is_zero, shifted, fraction);
@@ -1281,7 +1281,7 @@ bvt float_utilst::sticky_right_shift(
   {
     if(dist[stage]!=const_literal(false))
     {
-      bvt tmp=bv_utils.shift(result, bv_utilst::shiftt::LRIGHT, d);
+      bvt tmp=bv_utils.shift(result, bv_utilst::shiftt::SHIFT_LRIGHT, d);
 
       bvt lost_bits;