about summary refs log tree commit diff homepage
path: root/runtime/svcomp64/functions.c
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/svcomp64/functions.c')
-rw-r--r--runtime/svcomp64/functions.c9
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) {