diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index e9739285f236920e75fb0f1ea7e05acc6cdcb064..81189e5a19013ca4f3ff20a62e3c22502bd08878 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -1,33 +1,38 @@
 [package]
 name = "klee-examples"
 version = "0.2.0"
-authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
+authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
 
 [dependencies]
-klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+#klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+klee = {path =".."}
 panic-abort = "0.3.1"
 
 
-[dependencies.volatile-register]
-version = "0.3.0"
-
 [dependencies.cortex-m]
 version = "0.6.0"
 # #features = ["inline-asm", "klee-analysis"]
 
 [patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+#vcell = { path = "../../vcell" }
+#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
 volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
 #volatile-register = { path = "../../klee/volatile-register/" }
 cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
-#cortex-m = { path = "../../cortex-m" }
 
-# [dependencies.stm32f413]
-# version = "0.3.0"
-# path = "../stm32f413"
+[dependencies.volatile-register]
+version = "0.3.0"
+
+[dependencies.stm32f413]
+version = "0.3.0"
+path = "../../klee/stm32f413/"
+optional = true
 
-#[patch.crates-io]
-#cortex-m = { path = "../cortex-m" }
-#volatile-register = { version = "0.3.0", path = "../volatile-register" }
+[[examples]]
+name = "gpioa"
+path = "examples/gpioa.rs"
+#required-features = ["klee-device"] # seem to work only in [[bin]]
 
 [[bin]]
 name = "foo"
@@ -51,6 +56,5 @@ panic = "abort"
 lto = true
 
 [features]
-#klee-analysis = ["stm32f413/klee-analysis", "cortex-m/klee-analysis", "klee/klee-analysis"]
 klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
-#klee-replay = ["klee/klee-replay"]
+klee-device = ["stm32f413/klee-analysis"]
diff --git a/klee-examples/examples/gpioa.rs b/klee-examples/examples/gpioa.rs
new file mode 100644
index 0000000000000000000000000000000000000000..cf21409e755ec357983e5836402d9480c5433219
--- /dev/null
+++ b/klee-examples/examples/gpioa.rs
@@ -0,0 +1,23 @@
+#![no_std]
+#![no_main]
+
+extern crate cortex_m;
+extern crate klee;
+extern crate panic_abort;
+extern crate stm32f413;
+
+use core::ptr;
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let syst = peripherals.SYST;
+
+    let p = stm32f413::Peripherals::take().unwrap();
+    let gpioa = p.GPIOA;
+
+    if gpioa.moder.read().bits() == 0 {
+        let p =  Peripherals::take().unwrap();
+    }
+}
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
index 2d59b5de36689317ef7562e6c15278d2ccc47319..6febd18b0ff4190e9fa2b2dc225359e5994e20c3 100644
--- a/klee-examples/examples/modify.rs
+++ b/klee-examples/examples/modify.rs
@@ -3,6 +3,7 @@
 
 #[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::RW;
@@ -14,13 +15,13 @@ fn main() {
     unsafe {
         rw.modify(|r| {
             if r == 0 {
-                klee::abort();
+                panic!(); // rust compiler calls panic abort
             }
             0
         });
     }
 
     if rw.read() == 0 {
-        klee::abort();
+        klee::abort(); // we directly call the intrinsic abort
     }
 }
diff --git a/klee-examples/examples/registers.rs b/klee-examples/examples/registers.rs
index 6c93e98c07287632562193a337dbc8f7a50e5f9f..037ee4f4dfbbef85b1cb3110e90fb0c329aa8b23 100644
--- a/klee-examples/examples/registers.rs
+++ b/klee-examples/examples/registers.rs
@@ -1,8 +1,8 @@
 #![no_std]
 #![no_main]
 
-#[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::{RO, RW, WO};
diff --git a/klee-examples/examples/systick.rs b/klee-examples/examples/systick.rs
new file mode 100644
index 0000000000000000000000000000000000000000..266651a44a1a7479b9407b9366733e52ae3d83e3
--- /dev/null
+++ b/klee-examples/examples/systick.rs
@@ -0,0 +1,20 @@
+#![no_std]
+#![no_main]
+
+extern crate cortex_m;
+extern crate klee;
+extern crate panic_abort;
+
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let peripherals = Peripherals::take().unwrap();
+    let syst = peripherals.SYST;
+
+    if syst.rvr.read() == 0 {
+        if syst.cvr.read() == 0x21 {
+            panic!();
+        }
+    }
+}
diff --git a/klee-examples/src/foo.rs b/klee-examples/src/foo.rs
index 76ba4408a69b46af79ab1e7dab85fe3a47fedf1f..a86342d1a0c22d2c61e14915e621a19ee2c9b588 100644
--- a/klee-examples/src/foo.rs
+++ b/klee-examples/src/foo.rs
@@ -3,6 +3,7 @@
 
 #[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 use core::ptr;
 
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index 53d77066304ec81cfa97d9cc99f81160ecef4927..e281cd8d356b8864f3ebb784a2e481fa940bbddd 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -1,15 +1,11 @@
 #![no_std]
 #![no_main]
 
-#[macro_use]
 extern crate klee;
-
-#[cfg(not(feature = "klee-analysis"))]
 extern crate panic_abort;
 
 extern crate cortex_m;
 
-use core::ptr;
 use cortex_m::peripheral::Peripherals;
 
 #[no_mangle]
@@ -25,5 +21,4 @@ fn main() {
             klee::abort();
         };
     };
-
 }
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index f5a6faeabcc9b82b94375394983b0be5122427ce..3df905db95b2afa490d7009cefcd1adf30e3917e 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -39,8 +39,8 @@
 #![no_std]
 #![no_main]
 
-#[macro_use]
 extern crate klee;
+extern crate panic_abort;
 
 extern crate volatile_register;
 use volatile_register::RO;
@@ -51,7 +51,7 @@ fn main() {
 
     if rw.read() == 0 {
         if rw.read() == 0 {
-            panic!();
+            klee::abort();
         }
     }
 }