From 7169f935ee485501ea687e14b4e46b0298d58b27 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 21 Oct 2015 16:18:17 +0100
Subject: Change implementation of __VERIFIER_assume() so that if it's isn't
 satisfiable KLEE doesn't exit with an error.

---
 runtime/svcomp64/functions.c | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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) {
-- 
cgit 1.4.1