diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams1.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ea4032fbde38d50fdb39ac3163a04ada685440e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams1.scala
@@ -0,0 +1,24 @@
+object HigherOrderFunctionsMutableParams1 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => Unit, a: A): Unit = {
+    f(a)
+  }
+
+  def fImpl(a: A): Unit = {
+    a.x += 1
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl, a)
+    assert(a.x == 1)
+    app(fImpl, a)
+    assert(a.x == 2)
+    app(fImpl, a)
+    a.x
+  } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams2.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dbf3413855bc65f12f5380c49e58c5e7bd463933
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams2.scala
@@ -0,0 +1,22 @@
+object HigherOrderFunctionsMutableParams2 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def fImpl(a: A): BigInt = {
+    a.x += 1
+    a.x
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl, a)
+    app(fImpl, a)
+    app(fImpl, a)
+  } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams3.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c8dfc83bb1b9447d434dd1273b266247940ebcb5
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams3.scala
@@ -0,0 +1,26 @@
+object HigherOrderFunctionsMutableParams3 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def fImpl1(a: A): BigInt = {
+    a.x += 1
+    a.x
+  }
+  def fImpl2(a: A): BigInt = {
+    a.x += 10
+    a.x
+  }
+
+
+  def test(): BigInt = {
+    val a = A(0)
+    app(fImpl1, a)
+    app(fImpl2, a)
+    app(fImpl1, a)
+  } ensuring(_ == 12)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams4.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e379dfef4dd524b4955deaadfc071098033d467f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams4.scala
@@ -0,0 +1,25 @@
+object HigherOrderFunctionsMutableParams4 {
+
+  case class A(var x: BigInt)
+
+  def app(f: (A) => BigInt, a: A): BigInt = {
+    f(a)
+  }
+
+  def test(): BigInt = {
+    val a = A(0)
+    app((a2: A) => {
+      a2.x += 1
+      a2.x
+    }, a)
+    app((a2: A) => {
+      a2.x += 10
+      a2.x
+    }, a)
+    app((a2: A) => {
+      a2.x += 1
+      a2.x
+    }, a)
+  } ensuring(_ == 12)
+
+}