diff --git a/klee-examples/examples/cc_loop.rs b/klee-examples/examples/cc_loop.rs
new file mode 100644
index 0000000000000000000000000000000000000000..b3dcaaa42502092b912986525e24861360d65525
--- /dev/null
+++ b/klee-examples/examples/cc_loop.rs
@@ -0,0 +1,29 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    let mut j = 0;
+    for _i in 0..u {
+        j += 1;
+    }
+    j
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}
diff --git a/klee-examples/examples/cc_native_add.rs b/klee-examples/examples/cc_native_add.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6f272c7cb18c493032db082350f7055b4f6816b1
--- /dev/null
+++ b/klee-examples/examples/cc_native_add.rs
@@ -0,0 +1,23 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u + 1
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}
diff --git a/klee-examples/examples/cc_saturating.rs b/klee-examples/examples/cc_saturating.rs
new file mode 100644
index 0000000000000000000000000000000000000000..2ee2f410eb213c39366c0a61f4c7d93e1f963f28
--- /dev/null
+++ b/klee-examples/examples/cc_saturating.rs
@@ -0,0 +1,25 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ops::Add;
+
+use core::ptr;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 saturating
+fn f1(u: u8) -> u8 {
+    //if u < 255 { u + 1 } else { u } 
+    u.checked_add(1).unwrap_or(u)
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}
diff --git a/klee-examples/examples/cc_wrapping.rs b/klee-examples/examples/cc_wrapping.rs
new file mode 100644
index 0000000000000000000000000000000000000000..2689548b69eee9d8a0ad0d9c75946d02a2fac00b
--- /dev/null
+++ b/klee-examples/examples/cc_wrapping.rs
@@ -0,0 +1,25 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+ use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = symbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div( 100, u) }
+}
diff --git a/klee-examples/examples/foo.rs b/klee-examples/examples/foo.rs
index 4de0a258592bf481c37a6d5af15399deab7a69d6..83851e4253a333352f2c8badaea0918eac4151bd 100644
--- a/klee-examples/examples/foo.rs
+++ b/klee-examples/examples/foo.rs
@@ -13,7 +13,7 @@ fn main() {
     }
 }
 
-// add 1 and saturate
+// add 1 wrapping
 fn f1(u: u8) -> u8 {
     u.wrapping_add(1)
 }
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index 75ad8d974ebcba1d9a0b77efe5d998f420a26ece..f2b035b86c4ebda027d9143bdd5a5c50844c6991 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -9,11 +9,17 @@ mod ll;
 
 use core::mem;
 
-use cty::c_void;
+use cty::{c_int, c_void};
 
 #[doc(hidden)]
 pub use cstr_core::CStr;
 
+//extern "C" fn memcmp(cx: *const c_void, ct: *const c_void, n: size_t) -> c_int {
+#[no_mangle]
+pub fn memcmp(cx: *const c_void, ct: *const c_void, n: usize) -> c_int {
+    ::abort();
+}
+
 pub fn abort() -> ! {
     unsafe { ll::abort() }
 }