diff --git a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
index abc62eec0..14b9bc6a4 100644
--- a/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
+++ b/src/main/scala/viper/silver/ast/utility/BackendTypeFactories.scala
@@ -10,15 +10,78 @@ import viper.silver.ast.{Bool, Int, LocalVarDecl, BackendFunc, BackendType}
 case class BVFactory(size: Int) {
   lazy val typ = BackendType(s"bv${size}", s"(_ BitVec ${size})")
 
+  /**
+   * bit vector bitwise xor
+   */
   def xor(name: String) = BackendFunc(name, "bvxor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector bitwise bvxnor
+   */
+  def xnor(name: String) = BackendFunc(name, "bvxnor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector bitwise and
+   */
   def and(name: String) = BackendFunc(name, "bvand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector bitwise nand
+   */
+  def nand(name: String) = BackendFunc(name, "bvnand", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector bitwise or
+   */
   def or(name: String) = BackendFunc(name, "bvor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector bitwise nor
+   */
+  def nor(name: String) = BackendFunc(name, "bvnor", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector addition
+   */
   def add(name: String) = BackendFunc(name, "bvadd", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector subtraction
+   */
+  def sub(name: String) = BackendFunc(name, "bvsub", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector multiplication
+   */
   def mul(name: String) = BackendFunc(name, "bvmul", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector signed modulo
+   */
+  def smod(name: String) = BackendFunc(name, "bvsmod", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector unsigned division
+   */
+  def udiv(name: String) = BackendFunc(name, "bvudiv", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector unsigned remainder
+   */
+  def urem(name: String) = BackendFunc(name, "bvurem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector signed remainder
+   */
+  def srem(name: String) = BackendFunc(name, "bvsrem", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector shift left
+   */
   def shl(name: String) = BackendFunc(name, "bvshl", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
-  def shr(name: String) = BackendFunc(name, "bvshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector unsigned (logical) shift right
+   */
+  def lshr(name: String) = BackendFunc(name, "bvlshr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
+  /**
+   * bit vector signed (arithmetical) shift right
+   */
+  def ashr(name: String) = BackendFunc(name, "bvashr", typ, Seq(LocalVarDecl("x", typ)(), LocalVarDecl("y", typ)()))
 
+  /**
+   * bit vector bitwise not
+   */
   def not(name: String) = BackendFunc(name, "bvnot", typ, Seq(LocalVarDecl("x", typ)()))
+  /**
+   * bit vector unary minus
+   */
   def neg(name: String) = BackendFunc(name, "bvneg", typ, Seq(LocalVarDecl("x", typ)()))
 
   def from_int(name: String) = BackendFunc(name, s"(_ int2bv ${size})", typ, Seq(LocalVarDecl("x", Int)()))
@@ -71,4 +134,4 @@ case class FloatFactory(mant: Int, exp: Int, roundingMode: RoundingMode) {
 
   def from_bv(name: String) = BackendFunc(name, s"(_ to_fp ${exp} ${mant}) ", typ, Seq(LocalVarDecl("x", BVFactory(mant+exp).typ)()))
   def to_bv(name: String) = BackendFunc(name, s"(_ fp.to_sbv ${exp+mant}) ${roundingMode} ", BVFactory(mant+exp).typ, Seq(LocalVarDecl("x", typ)()))
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
index 361690f9f..3fe153f98 100644
--- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
@@ -167,6 +167,36 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi
     (wrapInProgram(Seq(assign, assertion1), Seq(), Seq(result_decl)), assertion1)
   }
 
+  def generateBvOpTest2() : Program = {
+    val bv23 = BVFactory(23)
+    val from_int = bv23.from_int("toBV23")
+    val two_lit = IntLit(2)()
+    val one_lit = IntLit(1) ()
+    val two = BackendFuncApp(from_int, Seq(two_lit))()
+    val one = BackendFuncApp(from_int, Seq(one_lit))()
+    val res_decl = LocalVarDecl("res", bv23.typ)()
+    val res = res_decl.localVar
+    wrapInProgram(
+      Seq(
+        LocalVarAssign(res, BackendFuncApp(bv23.xor("xorBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.xnor("xnorBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.and("andBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.nand("nandBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.or("orBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.nor("norBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.add("addBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.sub("subBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.mul("mulBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.smod("smodBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.srem("sremBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.udiv("udivBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.urem("uremBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.shl("shlBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.lshr("lshrBV23"), Seq(one, two))())(),
+        LocalVarAssign(res, BackendFuncApp(bv23.ashr("ashrBV23"), Seq(one, two))())(),
+      ), Seq(), Seq(res_decl))
+  }
+
   def wrapInProgram(stmts: Seq[Stmt], params: Seq[LocalVarDecl], vars: Seq[LocalVarDecl], fields: Seq[Field] = Seq()): Program = {
     val block = Seqn(stmts, vars)()
     val method = Method("test", params, Seq(), Seq(), Seq(), Some(block))()
@@ -229,6 +259,12 @@ trait BackendTypeTest extends FunSuite with Matchers with BeforeAndAfterAllConfi
     })
   }
 
+  test("bvOp2Success") {
+    val prog = generateBvOpTest2()
+    val res  = verifier.verify(prog)
+    assert(res == Success)
+  }
+
   test("floatOpSuccess") {
     val (prog, _) = generateFloatOpTest(true)
     val res  = verifier.verify(prog)