diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
new file mode 100644
index 0000000000000000000000000000000000000000..1ebbd7d29b14a7e098abc8ebad7625f5cfdb60f6
--- /dev/null
+++ b/klee-examples/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "klee-examples"
+version = "0.1.0"
+authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
+
+[dependencies]
+klee = {path=".."}
+
+[profile.release]
+debug = true
+panic = "abort"
+lto = true
\ No newline at end of file
diff --git a/klee-examples/examples/foo.rs b/klee-examples/examples/foo.rs
new file mode 100644
index 0000000000000000000000000000000000000000..78483d2a03e7968fb13df1ffc65323d960c83991
--- /dev/null
+++ b/klee-examples/examples/foo.rs
@@ -0,0 +1,25 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+#[no_mangle]
+fn main() {
+    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 {
+    100 / u
+}