diff options
Diffstat (limited to 'runtime/svcomp64/functions.c')
| -rw-r--r-- | runtime/svcomp64/functions.c | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/runtime/svcomp64/functions.c b/runtime/svcomp64/functions.c index 0fdae3bd..f8957e66 100644 --- a/runtime/svcomp64/functions.c +++ b/runtime/svcomp64/functions.c @@ -52,7 +52,14 @@ float __VERIFIER_nondet_float() { } void __VERIFIER_assume(int condition) { - klee_assume(condition); + // Guard the condition we assume so that if it is not + // satisfiable we don't flag up an error. Instead we'll + // just silently terminate this state. + if (condition) { + klee_assume(condition); + } else { + klee_silent_exit(0); + } } void __VERIFIER_assert(int cond) { |