diff --git a/testcases/malkis/Hardest.scala b/testcases/malkis/Hardest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2417f7db328157f3ed7a4d91b2280b72eb0702f1
--- /dev/null
+++ b/testcases/malkis/Hardest.scala
@@ -0,0 +1,32 @@
+import scala.collection.immutable.Set
+
+object Hardest {
+  def vc(
+    thread : Set[Int],
+    thread_A : Set[Int],
+    thread_A_2 : Set[Int],
+    thread_B_3 : Set[Int],
+    thread_C_2 : Set[Int],
+    thread_count : Int,
+    thread_count_2 : Int,
+    thread_t : Int,
+    thread_t_1 : Int,
+    nulll : Int
+  ) : Boolean = {
+    require(
+         thread_B_3.contains(thread_t_1)
+      && (thread_C_2 == Set.empty[Int] || 0 == 0)
+      && (thread_B_3 ** thread_C_2) == Set.empty[Int]
+      && (thread_A_2 ** thread_C_2) == Set.empty[Int]
+      && (thread_A_2 ** thread_B_3) == Set.empty[Int]
+      && ((thread_A_2 ++ thread_B_3 ++ thread_C_2) subsetOf thread)
+      && (thread_A_2.size <= 0)
+      && !thread.contains(nulll)
+      && (thread_A subsetOf thread)
+      && (thread_A.size <= thread_count)
+      && thread.contains(thread_t)
+    )
+    ((thread_A_2 ++ (thread_B_3 -- Set(thread_t_1))) ++
+     (thread_C_2 ++ Set(thread_t_1))) subsetOf thread
+  } ensuring(res => res)
+}