Try to fix the TravisCI build when using Z3 as the solver. The

``test/Feature/SolverTimeout.c`` test fails there.

The error message I see in TravisCI is

```
Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc"
Command 2 Result: -11
Command 2 Output:
Command 2 Stderr:
KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR: (location information missing) divide by zero
KLEE: NOTE: now ignoring this error at this location
0  klee            0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1  klee            0x0000000000da85c9
2  libpthread.so.0 0x00007fca19936cb0
3  libz3.so        0x00007fca19079826
4  librt.so.1      0x00007fca1747640c
5  libpthread.so.0 0x00007fca1992ee9a
6  libc.so.6       0x00007fca1776c38d clone + 109
```

The issue appears to be racey as I had to run several copies of KLEE in
parallel for the bug to occur using Z3 4.4.1. I managed to get a
coredump and got the backtrace from gdb for the crash which is

```
 #0  0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112
 #1  0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63
 #2  0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312
 #3  0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111
```

The crash appears to be in Z3 itself but I can't reproduce the issue when using the
version of Z3 from the master branch.

For now we simply workaround the issue by not running the
``test/Feature/SolverTimeout.c`` test when using Z3 as the solver.

We should revisit this issue when another stable release of Z3 is made.

1 files changed, 3 insertions, 0 deletions

diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c
index 2ef6d413..aa86a856 100644
--- a/test/Feature/SolverTimeout.c
+++ b/test/Feature/SolverTimeout.c
@@ -1,6 +1,9 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t1.bc
+// FIXME: This test occasionally fails when using Z3 4.4.1 but
+// not when using Z3 from the master branch. So disable the test for now.
+// REQUIRES: stp
 #include <stdio.h>
 
 int main() {