diff --git a/klee-examples/examples/cc_add.rs b/klee-examples/examples/cc_add.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d0e3e84f9b20f0cab50ec032bee316c3ebed2812
--- /dev/null
+++ b/klee-examples/examples/cc_add.rs
@@ -0,0 +1,32 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    // if u > 254 {
+    //     u
+    // } else {
+    //     u.wrapping_add(1)
+    // }
+    // // u.checked_add(1).unwrap_or(u)
+    u + 1
+}
+
+fn f2(u: u8) -> u8 {
+    // unsafe { unchecked_div( 100, u) }
+    100 / u
+}
diff --git a/klee-examples/examples/cc_contract.rs b/klee-examples/examples/cc_contract.rs
new file mode 100644
index 0000000000000000000000000000000000000000..99c7be9fd4d18c617a382f97d1bc0a4e88b24159
--- /dev/null
+++ b/klee-examples/examples/cc_contract.rs
@@ -0,0 +1,64 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    f1_check();
+    f2_check();
+    f2_f1_check();
+}
+
+// contract f1
+fn f1_pre(u: u8) -> bool {
+    true
+}
+
+fn f1_post(u: u8) -> bool {
+    u > 0
+}
+
+// check pre-post f1
+fn f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_pre(u));
+    let r = f1(u);
+    kassert!(f1_post(r));
+}
+
+fn f1(u: u8) -> u8 {
+    u.checked_add(1).unwrap_or(u)
+}
+
+// contract f2
+fn f2_pre(u: u8) -> bool {
+    u != 0
+}
+
+fn f2_post(u: u8) -> bool {
+    true
+}
+
+// check pre-post f2
+fn f2_check() {
+    let u = ksymbol!("u");
+    kassume(f2_pre(u));
+    let r = f2(u);
+    kassert!(f2_post(r));
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}
+
+// check f2_f1 composition
+fn f2_f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_post(u));
+    kassert!(f2_pre(u));
+}
diff --git a/klee-examples/examples/cc_contract_err.rs b/klee-examples/examples/cc_contract_err.rs
new file mode 100644
index 0000000000000000000000000000000000000000..d1d27aa17b05815ab39f6ed68c0bc34af21ee933
--- /dev/null
+++ b/klee-examples/examples/cc_contract_err.rs
@@ -0,0 +1,64 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    f1_check();
+    f2_check();
+    f2_f1_check();
+}
+
+// contract f1
+fn f1_pre(u: u8) -> bool {
+    true
+}
+
+fn f1_post(u: u8) -> bool {
+    u > 0
+}
+
+// check pre-post f1
+fn f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_pre(u));
+    let r = f1(u);
+    kassert!(f1_post(r));
+}
+
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+// contract f2
+fn f2_pre(u: u8) -> bool {
+    u != 0
+}
+
+fn f2_post(u: u8) -> bool {
+    true
+}
+
+// check pre-post f2
+fn f2_check() {
+    let u = ksymbol!("u");
+    kassume(f2_pre(u));
+    let r = f2(u);
+    kassert!(f2_post(r));
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}
+
+// check f2_f1 composition
+fn f2_f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_post(u));
+    kassert!(f2_pre(u));
+}
diff --git a/klee-examples/examples/cc_equivalence.rs b/klee-examples/examples/cc_equivalence.rs
new file mode 100644
index 0000000000000000000000000000000000000000..683b0451382d5e3b49eb92e98a587fe8246bcf33
--- /dev/null
+++ b/klee-examples/examples/cc_equivalence.rs
@@ -0,0 +1,25 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ops::Add;
+
+use core::ptr;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    kassert!(f1(u) == f1b(u));
+}
+
+fn f1(u: u8) -> u8 {
+    if u < 255 {
+        u + 1
+    } else {
+        u
+    }
+}
+
+fn f1b(u: u8) -> u8 {
+    u.checked_add(1).unwrap_or(u)
+}
diff --git a/klee-examples/examples/cc_loop.rs b/klee-examples/examples/cc_loop.rs
index b3dcaaa42502092b912986525e24861360d65525..87eea38df22796825e9a174b57e2b1196ea79dd6 100644
--- a/klee-examples/examples/cc_loop.rs
+++ b/klee-examples/examples/cc_loop.rs
@@ -3,16 +3,20 @@
 
 #[macro_use]
 extern crate klee;
+use klee::kassume;
 
 use core::ptr;
 use core::intrinsics::unchecked_div;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
+    kassume(u < 10);
+    //kassert!(f1(u) == f1b(u));
+    assert!(f1(u) == f1b(u));
 
-    unsafe {
-        ptr::read_volatile(&f2(f1(u)));
-    }
+    // unsafe {
+    //     ptr::read_volatile(&f2(f1(u)));
+    // }
 }
 
 // add 1 wrapping
@@ -24,6 +28,10 @@ fn f1(u: u8) -> u8 {
     j
 }
 
+fn f1b(u: u8) -> u8 {
+    u
+}
+
 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
index 6f272c7cb18c493032db082350f7055b4f6816b1..75ccba327b0f76fe759fe1706480179c22a8341f 100644
--- a/klee-examples/examples/cc_native_add.rs
+++ b/klee-examples/examples/cc_native_add.rs
@@ -6,14 +6,13 @@ extern crate klee;
 use core::ptr;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
 
     unsafe {
         ptr::read_volatile(&f2(f1(u)));
     }
 }
 
-// add 1 wrapping
 fn f1(u: u8) -> u8 {
     u + 1
 }
diff --git a/klee-examples/examples/cc_saturating.rs b/klee-examples/examples/cc_saturating.rs
index 2ee2f410eb213c39366c0a61f4c7d93e1f963f28..db43512120332cb94606180f849c632149ccf030 100644
--- a/klee-examples/examples/cc_saturating.rs
+++ b/klee-examples/examples/cc_saturating.rs
@@ -7,16 +7,15 @@ use core::ops::Add;
 use core::ptr;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("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)
 }
 
diff --git a/klee-examples/examples/cc_unchecked_div.rs b/klee-examples/examples/cc_unchecked_div.rs
new file mode 100644
index 0000000000000000000000000000000000000000..91935982ce9ca155458ae7a8ec3504c53880d585
--- /dev/null
+++ b/klee-examples/examples/cc_unchecked_div.rs
@@ -0,0 +1,24 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+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/cc_wrapping.rs b/klee-examples/examples/cc_wrapping.rs
index 2689548b69eee9d8a0ad0d9c75946d02a2fac00b..b8ad0483312cc62fe63c2e3fdac52d2c5e68f82e 100644
--- a/klee-examples/examples/cc_wrapping.rs
+++ b/klee-examples/examples/cc_wrapping.rs
@@ -5,21 +5,20 @@
 extern crate klee;
 
 use core::ptr;
- use core::intrinsics::unchecked_div;
+use core::intrinsics::unchecked_div;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("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) }
+    100 / u
 }
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index f2b035b86c4ebda027d9143bdd5a5c50844c6991..48b0dbfcfe9473d856a0f451d6d4a78c13754e6e 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -24,7 +24,7 @@ pub fn abort() -> ! {
     unsafe { ll::abort() }
 }
 
-pub fn assume(cond: bool) {
+pub fn kassume(cond: bool) {
     unsafe {
         ll::klee_assume(cond);
     }
@@ -32,7 +32,7 @@ pub fn assume(cond: bool) {
 
 #[doc(hidden)]
 #[inline]
-pub fn symbol<T>(name: &CStr) -> T {
+pub fn ksymbol<T>(name: &CStr) -> T {
     let mut t: T = unsafe { mem::uninitialized() };
     unsafe {
         ll::klee_make_symbolic(
@@ -45,9 +45,9 @@ pub fn symbol<T>(name: &CStr) -> T {
 }
 
 #[macro_export]
-macro_rules! symbol {
+macro_rules! ksymbol {
     ($name:expr) => {
-        $crate::symbol(unsafe {
+        $crate::ksymbol(unsafe {
             $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
         })
     }
diff --git a/rls1509755957780.log b/rls1509755957780.log
new file mode 100644
index 0000000000000000000000000000000000000000..a29dede1f0aa9fb441095f9c518bbd6a570dae8a
--- /dev/null
+++ b/rls1509755957780.log
@@ -0,0 +1,6 @@
+error: expected expression, found `+`
+  --> stdin:22:11
+   |
+22 |         j++;
+   |           ^
+