diff --git a/test/Floats/round.c b/test/Floats/round.c index 864a9524e6..228ce0b4fb 100644 --- a/test/Floats/round.c +++ b/test/Floats/round.c @@ -1,7 +1,11 @@ +// Disabling sanitizers because bitwuzla crashes with an assertion failure +// REQUIRES: not-asan +// REQUIRES: not-msan +// REQUIRES: not-ubsan // RUN: %clang %s -emit-llvm -O0 -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --libc=klee --fp-runtime --output-dir=%t.klee-out --exit-on-error %t1.bc > %t-output.txt 2>&1 -// RUN: FileCheck -input-file=%t-output.txt %s --dump-input=always --dump-input-filter=all +// RUN: FileCheck -input-file=%t-output.txt %s // REQUIRES: fp-runtime #include "klee/klee.h" #include diff --git a/test/Industry/CoverageErrorCall/od-4.c b/test/Industry/CoverageErrorCall/od-4.c index 9843d832e3..3374f0b5f0 100644 --- a/test/Industry/CoverageErrorCall/od-4.c +++ b/test/Industry/CoverageErrorCall/od-4.c @@ -1,9 +1,11 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla +// Disabling sanitizers because bitwuzla crashes with an assertion failure // REQUIRES: not-asan // REQUIRES: not-msan +// REQUIRES: not-ubsan // REQUIRES: not-darwin -// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=180 --64 --debug %s 2>&1 | FileCheck %s --dump-input=always --dump-input-filter=all +// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=900 --64 --debug %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable extern long __VERIFIER_nondet_long(void);