From 279dcc2bcecbecb3dfe550c2a5f9545f2e703696 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 8 Nov 2011 14:29:15 +0000
Subject: [PATCH] Will work on this at some point maybe... His VCs look trivial
to Z3(+BAPA?).
---
testcases/malkis/Hardest.scala | 32 ++++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)
create mode 100644 testcases/malkis/Hardest.scala
diff --git a/testcases/malkis/Hardest.scala b/testcases/malkis/Hardest.scala
new file mode 100644
index 000000000..2417f7db3
--- /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)
+}
--
GitLab