diff --git a/Cargo.toml b/Cargo.toml
index f32ad7fd5682331b3e97cfb274688887c15d0c62..8cdb97feab98fbeb5430766899de43b92ba57a22 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -6,12 +6,33 @@ edition = "2018"
 
 [dependencies]
 panic-halt = "0.2.0"
+cortex-m-semihosting = "0.3.5"
+lm3s6965 = "0.1.3"
+vcell = "0.1.2"
+
+[dependencies.panic-klee]
+git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
+version = "0.1.0"
 
 [dependencies.klee-sys]
-path = "../klee-sys"
+git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
+version = "0.1.0"
+
+[dependencies.cortex-m-rtfm]
+path = "../cortex-m-rtpro"
+
+[dependencies.cortex-m]
+version = "0.6.0"
+# #features = ["inline-asm", "klee-analysis"]
+
+[patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git", branch = "trustit" }
+# volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
+# cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
 
 [features] 
-klee-analysis = ["klee-sys/klee-analysis"]
+klee-analysis = ["klee-sys/klee-analysis", "vcell/klee-analysis", "cortex-m-rtfm/klee-analysis"]
 
 [profile.dev]
 panic = "abort"
diff --git a/examples/klee_test.rs b/examples/klee_test.rs
index 2dc2836ca0c6f519ba1bf369f67cf5ea0f91b57b..282d2bc6010e01b532776d01f51daa1c4dd14745 100644
--- a/examples/klee_test.rs
+++ b/examples/klee_test.rs
@@ -2,7 +2,7 @@
 #![no_main]
 
 #[cfg(feature = "klee-analysis")]
-use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+use panic_klee as _;
 
 #[cfg(not(feature = "klee-analysis"))]
 use panic_halt as _;
@@ -14,6 +14,8 @@ fn main() {
     panic!();
 }
 
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
 #[cfg(feature = "klee-analysis")]
 #[no_mangle]
 fn main() {
diff --git a/examples/vcell_test.rs b/examples/vcell_test.rs
new file mode 100644
index 0000000000000000000000000000000000000000..a362802829e95bc55acc70b80820bee05ad7a20b
--- /dev/null
+++ b/examples/vcell_test.rs
@@ -0,0 +1,30 @@
+#![no_std]
+#![no_main]
+
+#[cfg(feature = "klee-analysis")]
+use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
+
+#[cfg(feature = "klee-analysis")]
+use panic_klee as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+use panic_halt as _;
+
+#[cfg(not(feature = "klee-analysis"))]
+#[no_mangle]
+fn main() {
+    let mut a = 0;
+    panic!();
+}
+
+use vcell;
+#[cfg(feature = "klee-analysis")]
+#[no_mangle]
+fn main() {
+    let mut vc = vcell::VolatileCell::new(0u32);
+    match vc.get() {
+        2 => klee_abort!(),
+        1 => klee_abort!(),
+        _ => (),
+    };
+}