about summary refs log tree commit diff homepage
path: root/test/Merging
diff options
context:
space:
mode:
Diffstat (limited to 'test/Merging')
-rw-r--r--test/Merging/incomplete_merge.c20
1 files changed, 17 insertions, 3 deletions
diff --git a/test/Merging/incomplete_merge.c b/test/Merging/incomplete_merge.c
index 1962cfaa..bb5e4f37 100644
--- a/test/Merging/incomplete_merge.c
+++ b/test/Merging/incomplete_merge.c
@@ -16,6 +16,11 @@
 // CHECK: close merge:
 // CHECK: close merge:
 
+// This test merges branches with vastly different instruction counts.
+// The incomplete merging heuristic merges preemptively if a branch takes too long.
+// It might occur that the random branch selection completes the heavy branch first,
+// which results in the branches being merged completely.
+
 #include <klee/klee.h>
 
 int main(int argc, char **args) {
@@ -31,15 +36,24 @@ int main(int argc, char **args) {
   if (a == 0) {
     klee_open_merge();
 
+    for (int i = 0; i < 5; ++i){
+      foo += 2;
+    }
     if (x == 1) {
-      foo = 5;
+      foo += 5;
     } else if (x == 2) {
-      foo = 6;
+      for (int i = 0; i < 10; ++i) {
+        foo += foo;
+      }
     } else {
-      foo = 7;
+      foo += 7;
     }
 
     klee_close_merge();
+  } else if (a == 1) {
+    foo = 4;
+  } else {
+    foo = 3;
   }
   klee_close_merge();