diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index 8d0bc899fc91ec186278a7a641c7eaa279e869d2..f451fb244198a0adf03ddffe47e2d8f018af14f5 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -1,3 +1,101 @@
+// > cargo klee --bin peripheral -r -k -g -v --release
+// ...
+// KLEE: done: total instructions = 33
+// KLEE: done: completed paths = 1
+// KLEE: done: generated tests = 1
+//
+// The example, has just one path, leading up to an abort.
+// The reason is that the progam unconditionally will panic, as
+// taking the peripheral is only only allowed once (for soundness).
+// (Internally this in tracked by a state variable.)
+//
+// This is very good news, that KLEE will detect the error at compile time.
+//
+// Let's remove the error to see if the example code is correct.
+// (comment out the second `take`)
+//
+// > cargo klee --bin peripheral -r -k -g -v --release
+//
+// KLEE: ERROR: src/peripheral.rs:104: divide by zero
+// KLEE: NOTE: now ignoring this error at this location
+//
+// KLEE: done: total instructions = 85
+// KLEE: done: completed paths = 2
+// KLEE: done: generated tests = 2
+//
+//(gdb) shell ls klee-last
+// assembly.ll  info  messages.txt  run.istats  run.stats  test000001.div.err  test000001.kquery  test000001.ktest  test000002.ktest  warnings.txt
+//
+// So we see that test000001.ktest was causing a division error,
+// the other test case passed
+//
+// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
+// (gdb) run
+// ...
+// Program received signal SIGFPE, Arithmetic exception.
+// 0x00005555555551b0 in main () at src/peripheral.rs:104
+// 104             let some_time_quota = unchecked_div(a, c - b);
+//
+// Let's look at the actual test
+// (gdb) shell ktest-tool klee-last/test000001.ktest
+// ktest file : 'klee-last/test000001.ktest'
+// args       : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/peripheral-d1d6043ca4c81fef.ll']
+// num objects: 5
+// object 0: name: 'PRIMASK'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// object 2: name: 'vcell'
+// object 2: size: 4
+// object 2: data: b'\x00\x00\x00\x00'
+// object 2: hex : 0x00000000
+// object 2: int : 0
+// object 2: uint: 0
+// object 2: text: ....
+// object 3: name: 'vcell'
+// object 3: size: 4
+// object 3: data: b'\x00\x00\x00\x00'
+// object 3: hex : 0x00000000
+// object 3: int : 0
+// object 3: uint: 0
+// object 3: text: ....
+// object 4: name: 'vcell'
+// object 4: size: 4
+// object 4: data: b'\x00\x00\x00\x00'
+// object 4: hex : 0x00000000
+// object 4: int : 0
+// object 4: uint: 0
+// object 4: text: ....
+//
+// In order to analyze hardware dependent code, hardware access are treated
+// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
+// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
+// might in the future change to giving the address to the register instead.
+//
+// A breakdown of the example:
+// Behind the scenes the PRIMASK register is accessed, and given concrete value.
+// This access is along the happy path towards the error, so any value would
+// suffice (in this case 0x00000000 was selected by KLEE).
+//
+// The first `vcell` access: was done when enabling the cycle counter.
+// The rest of accesses stem from reading `a`, `b`, and `c`.
+// Critical here is that KLEE spots that `(c - b) = 0`, leading up to a division
+// by zero error (satisfied by `c` and `b` set to 0x00000000)
+//
+// Notice here, that this error is spotted EVEN while we are telling
+// Rust to use the primitive (intrinsic) division for performance.
+//
+#![feature(core_intrinsics)] // we use intrinsic division
 #![no_std]
 #![no_main]
 
@@ -8,17 +106,18 @@ extern crate cortex_m;
 
 use cortex_m::peripheral::Peripherals;
 
+use core::{intrinsics::unchecked_div, ptr::read_volatile};
+
 #[no_mangle]
 fn main() {
     let peripherals = Peripherals::take().unwrap();
     let mut dwt = peripherals.DWT;
     dwt.enable_cycle_counter();
+    let a = dwt.cyccnt.read();
+    let b = dwt.cyccnt.read();
+    let c = dwt.cyccnt.read();
     unsafe {
-        dwt.ctrl.write(0);
+        let some_time_quota = unchecked_div(a, c - b);
+        read_volatile(&some_time_quota); // prevent optization
     }
-    if dwt.ctrl.read() == 0 {
-        if dwt.ctrl.read() == 0 {
-            klee::kabort!();
-        };
-    };
 }
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index a5f247c58ec34e6efba8acbded37ca16d2ffbf9e..f16ef61e37b6d8566c84513f76cbd89945f8356c 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -1,40 +1,85 @@
-//! showcase volatile register
-//!
-//! $ cargo klee --bin register -r -g -k
-//! ...
-//! 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
-//! rust_begin_unwind (_info=0x7fffffffd678)
-//!    at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:66
-//!            unsafe { intrinsics::abort() }
-//! (gdb) backtrace
-//! #0  rust_begin_unwind (_info=0x7fffffffd678)
-//!    at /home/pln/.cargo/git/checkouts/cargo-klee-8f30fda3bd23bb30/68dc73d/src/lang_items.rs:6
-//! #1  0x000055555555531c in core::panicking::panic_fmt () at src/libcore/panicking.rs:95
-//! #2  0x000055555555539b in core::panicking::panic () at src/libcore/panicking.rs:59
-//! #3  0x00005555555552a6 in main () at src/main2.rs:54
-//! (gdb) q
-//! A debugging session is active.
-//!
-//!        Inferior 1 [process 25893] will be killed.
-//! $ ktest-tool --write-int target/debug/deps/klee-last/test000003.ktest
-//! ktest file : 'target/debug/deps/klee-last/test000003.ktest'
-//! args       : ['/home/pln/rust/cargo-klee/klee-examples/target/debug/deps/main2-2a0fc03ce12ab528.ll']
-//! num objects: 2
-//! object    0: name: b'register'
-//! object    0: size: 4
-//! object    0: data: 0
-//! object    1: name: b'register'
-//! object    1: size: 4
-//! object    1: data: 0
+// showcase volatile register
+// This is the underlying abstraction to all register accesses using the
+// embedded Rust ecosystem.
+//
+// When analyzed by KLEE, we make the return value symbolic, thus each access
+// givs a new unique symbol. Even if we write a value to it, the next read
+// will still be treated as a new symbol. That might be overly pessimistic
+// but is a safe approximation for the worst case behavior of the hardware.
+//
+// > cargo klee --bin register --release
+// ...
+// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.2/src/lib.rs:49: abort failure
+// KLEE: NOTE: now ignoring this error at this location
+
+// KLEE: done: total instructions = 33
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+//
+// > ls target/release/deps/klee-last/
+// assembly.ll  info  messages.txt  run.istats  run.stats  test000001.ktest  test000002.ktest  test000003.abort.err  test000003.kquery  test000003.ktest  warnings.txt
+//
+// We see that KLEE spoted the test3 hits unreachable (and thus panics)
+//
+// Let's look at the test cases separately:
+//
+// test1 passed:
+// ktest-tool target/release/deps/klee-last/test000001.ktest
+// ktest file : 'target/release/deps/klee-last/test000001.ktest'
+// args       : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// num objects: 1
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+// If the first read of the register is not 1 then we are ok.
+//
+// The second test also passed.
+// ktest-tool target/release/deps/klee-last/test000002.ktest
+// ktest file : 'target/release/deps/klee-last/test000002.ktest'
+// args       : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// num objects: 2
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x01\x00\x00\x00'
+// object 0: hex : 0x01000000
+// object 0: int : 1
+// object 0: uint: 1
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x00\x00\x00\x00'
+// object 1: hex : 0x00000000
+// object 1: int : 0
+// object 1: uint: 0
+// object 1: text: ....
+// Here we are saved by the second reading of the register NOT giving
+// returning 2.
+//
+// The third test gives the error.
+// ktest-tool target/release/deps/klee-last/test000003.ktest
+// ktest file : 'target/release/deps/klee-last/test000003.ktest'
+// args       : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
+// num objects: 2
+// object 0: name: 'vcell'
+// object 0: size: 4
+// object 0: data: b'\x01\x00\x00\x00'
+// object 0: hex : 0x01000000
+// object 0: int : 1
+// object 0: uint: 1
+// object 0: text: ....
+// object 1: name: 'vcell'
+// object 1: size: 4
+// object 1: data: b'\x02\x00\x00\x00'
+// object 1: hex : 0x02000000
+// object 1: int : 2
+// object 1: uint: 2
+// object 1: text: ....
+//
+// The first read gives 1, the second 2, and we hit unreacable.
 
 #![no_std]
 #![no_main]
@@ -43,15 +88,20 @@ extern crate klee;
 extern crate panic_abort;
 
 extern crate volatile_register;
-use volatile_register::RO;
+use volatile_register::RW;
 
 #[no_mangle]
 fn main() {
-    let rw: RO<u32> = unsafe { core::mem::uninitialized() };
+    // we emulate a read/write hardware register (rw)
+    let rw: RW<u32> = unsafe { core::mem::MaybeUninit::uninit().assume_init() };
 
-    if rw.read() == 0 {
-        if rw.read() == 0 {
-            klee::kabort!();
+    // reading will render a symbolic value of type u32
+    if rw.read() == 1 {
+        // we emulate a write to the hardware register
+        unsafe { rw.write(0) };
+        // this read is still treated as a new symbolic value of type u32
+        if rw.read() == 2 {
+            unreachable!();
         }
     }
 }