diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 2668b3ccd9fd35ef5b23f7810abad914a82bcdfe..2418d2b02770b72c3a6f3a4f625459da8a2d2402 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -17,7 +17,9 @@ version = "0.6.0"
 
 [patch.crates-io]
 volatile-register = { git = "https://gitlab.henriktjader.com/pln/volatile-register.git", branch = "klee-analysis" }
-cortex-m = { git = "https://github.com/perlindgren/cortex-m.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"
@@ -50,5 +52,5 @@ lto = true
 
 [features]
 #klee-analysis = ["stm32f413/klee-analysis", "cortex-m/klee-analysis", "klee/klee-analysis"]
-klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis"]
+klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
 #klee-replay = ["klee/klee-replay"]
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
new file mode 100644
index 0000000000000000000000000000000000000000..2d59b5de36689317ef7562e6c15278d2ccc47319
--- /dev/null
+++ b/klee-examples/examples/modify.rs
@@ -0,0 +1,26 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+#[no_mangle]
+fn main() {
+    let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+
+    unsafe {
+        rw.modify(|r| {
+            if r == 0 {
+                klee::abort();
+            }
+            0
+        });
+    }
+
+    if rw.read() == 0 {
+        klee::abort();
+    }
+}
diff --git a/klee-examples/examples/registers.rs b/klee-examples/examples/registers.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6c93e98c07287632562193a337dbc8f7a50e5f9f
--- /dev/null
+++ b/klee-examples/examples/registers.rs
@@ -0,0 +1,32 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate volatile_register;
+use volatile_register::{RO, RW, WO};
+
+#[no_mangle]
+fn main() {
+    let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+    let ro: RO<u32> = unsafe { core::mem::uninitialized() };
+    let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+
+    unsafe { wo.write(2) };
+
+    if rw.read() == 0 {
+        unsafe {
+            rw.write(0);
+        }
+        if rw.read() == 0 {
+            panic!();
+        }
+    }
+
+    if ro.read() == 0 {
+        if ro.read() == 0 {
+            panic!();
+        }
+    }
+}
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index 1912ea79fc85280835893f9db1721429f061f9da..346cdfed9b406200fc2f2c00c1577d30fd91ded9 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -17,16 +17,16 @@ fn main() {
     let peripherals = Peripherals::take().unwrap();
     let mut dwt = peripherals.DWT;
     dwt.enable_cycle_counter();
-    unsafe {
-        dwt.ctrl.write(0);
-    }
-    if dwt.ctrl.read() == 0 {
-        if dwt.ctrl.read() == 0 {
-            klee::abort();
-        };
-    };
+    // unsafe {
+    //     dwt.ctrl.write(0);
+    // }
+    // if dwt.ctrl.read() == 0 {
+    //     if dwt.ctrl.read() == 0 {
+    //         klee::abort();
+    //     };
+    // };
 
-    unsafe {
-        ptr::read_volatile(&dwt);
-    }
+    // unsafe {
+    //     ptr::read_volatile(&dwt);
+    // }
 }
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index 5a771fa0a98425041ac1319e7c035ed68dfdbd0f..f5a6faeabcc9b82b94375394983b0be5122427ce 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -1,14 +1,14 @@
 //! showcase volatile register
-//! 
+//!
 //! $ cargo klee --bin register -r -g
 //! ...
 //! Reading symbols from register.replay...done.
-//! 
+//!
 //! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
 //! (gdb) run
 //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay
 //! [Inferior 1 (process 25074) exited with code 01]
-//! 
+//!
 //! (gdb) set env KTEST_FILE=klee-last/test000003.ktest
 //! (gdb) run
 //! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/release/deps/main2.replay