diff --git a/Cargo.toml b/Cargo.toml
index ec8aee6f6378a59e2683fcff067db208306900ce..b39720d1b81b1914f2551fc873986d276ba9d05a 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -40,9 +40,6 @@ optional = true
 vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
 #vcell = { path = "../vcell" }
 
-#volatile-register = { git = "https://github.com/perlindgren/volatile-register.git", branch = "trustit" }
-#volatile-register = { path = "../volatile-register" }
-
 cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "trustit" }
 #cortex-m = { path = "../cortex-m" }
 
@@ -52,12 +49,11 @@ cortex-m-rt = { path = "../cortex-m-rt" }
 [features] 
 klee-analysis = [ 
     "vcell/klee-analysis",
-#    "volatile-register/klee-analysis", 
     "cortex-m/klee-analysis", 
     "cortex-m-rt/klee-analysis" 
     ]
 inline-asm = ["cortex-m/inline-asm"]
-rtpro = [ "cortex-m-rtfm/klee-analysis", "lm3s6965" ]
+rtpro = [ "cortex-m-rtfm/klee-analysis", "cortex-m-rt/rtpro", "lm3s6965" ]
 
 [profile.dev]
 panic = "abort"
diff --git a/examples/rtfm_init.rs b/examples/rtfm_init.rs
new file mode 100644
index 0000000000000000000000000000000000000000..e07956ef0129c7603b213d6f0e63ef805d099d4e
--- /dev/null
+++ b/examples/rtfm_init.rs
@@ -0,0 +1,46 @@
+//! examples/init.rs
+
+// #![deny(unsafe_code)]
+// #![deny(warnings)]
+#![no_main]
+#![no_std]
+
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
+
+#[rtfm::app(device = lm3s6965)]
+const APP: () = {
+    #[init]
+    fn init(cx: init::Context) {
+        static mut X: u32 = 0;
+
+        // // Safe access to local `static mut` variable
+        // let _x: &'static mut u32 = X;
+        // if cfg!(feature = "klee-analysis") {
+        //     fn_to_test();
+        // } else {
+        //     hprintln!("init").unwrap();
+        //     debug::exit(debug::EXIT_SUCCESS);
+        // }
+    }
+};
+
+// #[cfg(feature = "klee-analysis")]
+// fn fn_to_test() {
+//     let mut a = 0;
+//     klee_make_symbolic!(&mut a, "a");
+//     match a {
+//         0 => klee_abort!(),
+//         1 => klee_abort!(),
+//         2 => panic!(),
+//         3 => panic!("3"), // just one instance of panic! will be spotted
+//         4 => klee_assert!(false),
+//         5 => klee_assert_eq!(false, true),
+//         6 => klee_assert_eq!(false, true),
+//         _ => (),
+//     };
+//     panic!("at end"); // just one instane of panic! will be spotted
+// }
+
+// #[cfg(not(feature = "klee-analysis"))]
+// fn fn_to_test() {}