diff --git a/smt/expr.cpp b/smt/expr.cpp
index 70353e8a1..e7107570a 100644
--- a/smt/expr.cpp
+++ b/smt/expr.cpp
@@ -497,6 +497,10 @@ bool expr::isSignExt(expr &val) const {
   return isUnOp(val, Z3_OP_SIGN_EXT);
 }
 
+bool expr::isAShr(expr &a, expr &b) const {
+  return isBinOp(a, b, Z3_OP_BASHR);
+}
+
 bool expr::isAnd(expr &a, expr &b) const {
   return isBinOp(a, b, Z3_OP_AND);
 }
@@ -1851,6 +1855,15 @@ expr expr::extract(unsigned high, unsigned low, unsigned depth) const {
       return val.sext(high - val_bits + 1);
     }
   }
+  {
+    expr a, b;
+    if (isAShr(a, b)) {
+      uint64_t shift;
+      if (b.isUInt(shift) && high + shift < a.bits()) {
+        return a.extract(high + shift, low + shift);
+      }
+    }
+  }
   {
     expr a, b;
     if (isConcat(a, b)) {
diff --git a/smt/expr.h b/smt/expr.h
index 038613e7c..5c139bb65 100644
--- a/smt/expr.h
+++ b/smt/expr.h
@@ -135,6 +135,7 @@ class expr {
   bool isConcat(expr &a, expr &b) const;
   bool isExtract(expr &e, unsigned &high, unsigned &low) const;
   bool isSignExt(expr &val) const;
+  bool isAShr(expr &a, expr &b) const;
   bool isAnd(expr &a, expr &b) const;
   bool isNot(expr &neg) const;
   bool isAdd(expr &a, expr &b) const;