about summary refs log tree commit diff homepage
path: root/runtime/Intrinsic/klee_range.c
diff options
context:
space:
mode:
Diffstat (limited to 'runtime/Intrinsic/klee_range.c')
-rw-r--r--runtime/Intrinsic/klee_range.c5
1 files changed, 3 insertions, 2 deletions
diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c
index 59d1a05e..5da6a7a5 100644
--- a/runtime/Intrinsic/klee_range.c
+++ b/runtime/Intrinsic/klee_range.c
@@ -13,12 +13,13 @@
 int klee_range(int start, int end, const char* name) {
   int x;
 
-  assert(start < end);
+  if (start >= end)
+    klee_report_error(__FILE__, __LINE__, "invalid range", "user");
 
   if (start+1==end) {
     return start;
   } else {
-    klee_make_symbolic_name(&x, sizeof x, name); 
+    klee_make_symbolic(&x, sizeof x, name); 
 
     /* Make nicer constraint when simple... */
     if (start==0) {