diff --git a/test/Feature/ubsan/ubsan_alignment-assumption.c b/test/Feature/ubsan/ubsan_alignment-assumption.c
index b48929ac01..d18f2a284c 100644
--- a/test/Feature/ubsan/ubsan_alignment-assumption.c
+++ b/test/Feature/ubsan/ubsan_alignment-assumption.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
index 587c510814..d0b5c03abe 100644
--- a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
+++ b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
index 37eb09278a..4fde8921b6 100644
--- a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
+++ b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_array_bounds.c b/test/Feature/ubsan/ubsan_array_bounds.c
index 626d016baa..ba4e7b5c5e 100644
--- a/test/Feature/ubsan/ubsan_array_bounds.c
+++ b/test/Feature/ubsan/ubsan_array_bounds.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=array-bounds -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_bool.c b/test/Feature/ubsan/ubsan_bool.c
index 4c2a9dbbee..360af183e8 100644
--- a/test/Feature/ubsan/ubsan_bool.c
+++ b/test/Feature/ubsan/ubsan_bool.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=bool -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/Feature/ubsan/ubsan_builtin.c
index 85603646d5..72ff73da24 100644
--- a/test/Feature/ubsan/ubsan_builtin.c
+++ b/test/Feature/ubsan/ubsan_builtin.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=builtin -w -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_enum.c b/test/Feature/ubsan/ubsan_enum.c
index d6422fcbe5..1c79629ac6 100644
--- a/test/Feature/ubsan/ubsan_enum.c
+++ b/test/Feature/ubsan/ubsan_enum.c
@@ -1,6 +1,8 @@
 // RUN: %clangxx %s -fsanitize=enum -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_float_cast_overflow.c b/test/Feature/ubsan/ubsan_float_cast_overflow.c
index 749a340eee..6f17c6fa59 100644
--- a/test/Feature/ubsan/ubsan_float_cast_overflow.c
+++ b/test/Feature/ubsan/ubsan_float_cast_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=float-cast-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
@@ -8,6 +10,8 @@ int main() {
   float f = 0x7fffff80;
   volatile int result;
 
+  // TODO: uncomment when support for floating points is integrated
+
   //  klee_make_symbolic(&f, sizeof(f), "f");
 
   // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: float-cast-overflow
diff --git a/test/Feature/ubsan/ubsan_float_divide_by_zero.c b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
index eec443938b..848571909a 100644
--- a/test/Feature/ubsan/ubsan_float_divide_by_zero.c
+++ b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
@@ -1,12 +1,16 @@
 // RUN: %clang %s -fsanitize=float-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .div.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
 int main() {
   float x = 1.0;
 
+  // TODO: uncomment when support for floating points is integrated
+
   //  klee_make_symbolic(&x, sizeof(x), "x");
   //  klee_assume(x != 0.0);
 
diff --git a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
index d8e99e54f2..9b33466457 100644
--- a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
+++ b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-integer-sign-change -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
index 3d6ffcd1ec..cc511f7f12 100644
--- a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-signed-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
index 5421d10f0a..b90fac70e5 100644
--- a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-unsigned-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
index ff5458abae..c33bab38e7 100644
--- a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
+++ b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
@@ -1,6 +1,10 @@
 // RUN: %clang %s -fsanitize=integer-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-div-zero=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
+
+#include "klee/klee.h"
 
 #if defined(__SIZEOF_INT128__) && !defined(_WIN32)
 typedef __int128 intmax;
diff --git a/test/Feature/ubsan/ubsan_nonnull_attribute.c b/test/Feature/ubsan/ubsan_nonnull_attribute.c
index 0e1c841146..a98aeaddfe 100644
--- a/test/Feature/ubsan/ubsan_nonnull_attribute.c
+++ b/test/Feature/ubsan/ubsan_nonnull_attribute.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_null.c b/test/Feature/ubsan/ubsan_null.c
index 5f3a516fc7..f5ad6fdf63 100644
--- a/test/Feature/ubsan/ubsan_null.c
+++ b/test/Feature/ubsan/ubsan_null.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=null -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_arg.c b/test/Feature/ubsan/ubsan_nullability_arg.c
index 72cb79aaff..c739364910 100644
--- a/test/Feature/ubsan/ubsan_nullability_arg.c
+++ b/test/Feature/ubsan/ubsan_nullability_arg.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-arg -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_assign.c b/test/Feature/ubsan/ubsan_nullability_assign.c
index 84421bb7ac..eaf58a65d3 100644
--- a/test/Feature/ubsan/ubsan_nullability_assign.c
+++ b/test/Feature/ubsan/ubsan_nullability_assign.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-assign -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_return.c b/test/Feature/ubsan/ubsan_nullability_return.c
index 3e1a76d305..25b2b5e0cd 100644
--- a/test/Feature/ubsan/ubsan_nullability_return.c
+++ b/test/Feature/ubsan/ubsan_nullability_return.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-return -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
index acf551bc6b..dcbba073a3 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
index 529c0d11b2..cb1267423f 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
index dc9ff50fab..20286bcc0a 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
@@ -12,6 +14,7 @@ int main() {
   volatile char *result;
 
   klee_make_symbolic(&address, sizeof(address), "address");
+  klee_assume(address != 0);
 
   char *ptr = (char *)address;
 
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
index 29df382334..301952b980 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
index be15628c2e..123034b585 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_return.c b/test/Feature/ubsan/ubsan_return.c
index 3e9c8ccb8a..c2327db4c3 100644
--- a/test/Feature/ubsan/ubsan_return.c
+++ b/test/Feature/ubsan/ubsan_return.c
@@ -1,6 +1,8 @@
 // RUN: %clangxx %s -fsanitize=return -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
index d8fd661c00..f2a1c6e4cd 100644
--- a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
+++ b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=returns-nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_shift_base.c b/test/Feature/ubsan/ubsan_shift_base.c
index 31d87f43e1..2da7158220 100644
--- a/test/Feature/ubsan/ubsan_shift_base.c
+++ b/test/Feature/ubsan/ubsan_shift_base.c
@@ -1,6 +1,14 @@
-// RUN: %clang %s -fsanitize=shift -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: %clang %s -fsanitize=shift-base -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+//
+// There may be 2 or 3 test cases depending on the search heuristic, so we don't check the number of tests.
+// For example, 2 test cases may be as follows:
+// (1) b <= 31 without overflow, (2) a > 0 and b > 31 with overflow
+// For example, 3 test cases may be as follows:
+// (1) a = 0 and b > 31 without overflow, (2) b < 31 without overflow, (3) a > 0 and b > 31 with overflow
+//
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_shift_exponent.c b/test/Feature/ubsan/ubsan_shift_exponent.c
index 1716ecb9bb..548ebb66c0 100644
--- a/test/Feature/ubsan/ubsan_shift_exponent.c
+++ b/test/Feature/ubsan/ubsan_shift_exponent.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=shift-exponent -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_signed_integer_overflow.c b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
index 306d0935cb..df798e7957 100644
--- a/test/Feature/ubsan/ubsan_signed_integer_overflow.c
+++ b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=signed-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 5
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 4
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unreachable.c b/test/Feature/ubsan/ubsan_unreachable.c
index 56de8e617d..76e2e9091e 100644
--- a/test/Feature/ubsan/ubsan_unreachable.c
+++ b/test/Feature/ubsan/ubsan_unreachable.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=unreachable -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
index fb90d97fb3..a11c8d07a7 100644
--- a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
+++ b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 5
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 4
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unsigned_shift_base.c b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
index d08bfe160a..92c6135345 100644
--- a/test/Feature/ubsan/ubsan_unsigned_shift_base.c
+++ b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
@@ -2,7 +2,9 @@
 
 // RUN: %clang %s -fsanitize=unsigned-shift-base -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_vla_bound.c b/test/Feature/ubsan/ubsan_vla_bound.c
index 24a95d17c7..a057c62c10 100644
--- a/test/Feature/ubsan/ubsan_vla_bound.c
+++ b/test/Feature/ubsan/ubsan_vla_bound.c
@@ -1,6 +1,9 @@
 // RUN: %clang %s -fsanitize=vla-bound -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 3
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .model.err | wc -l | grep 1
 
 #include "klee/klee.h"