aboutsummaryrefslogtreecommitdiffhomepage
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();