diff options
Diffstat (limited to 'test/Merging/incomplete_merge.c')
-rw-r--r-- | test/Merging/incomplete_merge.c | 20 |
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(); |