about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-10-21 16:18:17 +0100
committerDan Liew <daniel.liew@imperial.ac.uk>2015-10-21 16:18:17 +0100
commit7169f935ee485501ea687e14b4e46b0298d58b27 (patch)
treebe5e41c334cccec185063da2dc2132afc6af91a0
parent2f9b4c233bbb49c17c506dd424801068cb8003df (diff)
downloadklee-svcomp_32bit.tar.gz
Change implementation of __VERIFIER_assume() so that if it's isn't svcomp_32bit
satisfiable KLEE doesn't exit with an error.
-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) {