diff --git a/app/Cargo.toml b/app/Cargo.toml
index 24cf25908d93e70981128131d39ed8d9b95cd885..6ac79bf1dc3f32baa97c1e1a40f31b77ec61eb82 100644
--- a/app/Cargo.toml
+++ b/app/Cargo.toml
@@ -5,6 +5,9 @@ readme = "README.md"
 name = "app"
 version = "0.1.0"
 
+[patch.crates-io]
+cortex-m = { path = "../cortex-m" }
+
 [dependencies.cortex-m]
 version = "0.5.8"
 features = ["inline-asm"]
diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 1ebbd7d29b14a7e098abc8ebad7625f5cfdb60f6..d9004feadd34ed4f6967ab5f9af8c5b30cc6f8df 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -6,6 +6,14 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io
 [dependencies]
 klee = {path=".."}
 
+[patch.crates-io]
+cortex-m = { path = "../cortex-m" }
+
+[dependencies.cortex-m]
+version = "0.5.8"
+features = ["inline-asm", "klee_analysis"]
+
+
 [profile.release]
 debug = true
 panic = "abort"
diff --git a/klee-examples/examples/cc_lab4_contract.rs b/klee-examples/examples/cc_lab4_contract.rs
index 44da140ef4b306b7301e2014d82467bb70c33e91..01b755d3dd9ac566523b50da19b60c1aee55e2db 100644
--- a/klee-examples/examples/cc_lab4_contract.rs
+++ b/klee-examples/examples/cc_lab4_contract.rs
@@ -10,23 +10,28 @@ static mut PLAIN: [u8; 132] = [0; 132];
 
 static ABC: [u32; 4] = [0x9fdd9158, 0x85715808, 0xac73323a, 0];
 static CODED: [u32; 132] = [
-    0x015e7a47, 0x2ef84ebb, 0x177a8db4, 0x1b722ff9, 0x5dc7cff0, 0x5dc9dea6, 0x1da0c15a, 0xe4c236a2,
-    0x3d16b0d0, 0x1f397842, 0xaae0d2ba, 0x11246674, 0x0845317f, 0xd5512dad, 0xb6184977, 0xd293a53e,
-    0x7d9c2716, 0xd917eae6, 0xd8852384, 0x286e46f9, 0xce566029, 0xcefe7daf, 0x62d726d4, 0x0dbaeb2d,
-    0x95f57c60, 0xed515141, 0x29b77d0f, 0x9f7b8d0c, 0x45a8395a, 0xfead2b72, 0x883d434c, 0xed8ddf60,
-    0xe51e65e4, 0x19bf6bb1, 0xfeb505ec, 0x662aa23c, 0xf6827cf8, 0xd1dc7a5c, 0x4fa5b066, 0x7ddd25a4,
-    0xa8ba8e8a, 0x72846227, 0xf8f636fb, 0x2b389a9c, 0xe4038bf6, 0x6e169877, 0xad028132, 0x84dbfe8c,
-    0x243762ff, 0x59c8f80c, 0xb6e0db4b, 0xedb8cab7, 0xcd4b39f6, 0xaf263741, 0x18d9965f, 0x1ab1f037,
-    0x5b458792, 0xc94d960d, 0xd45cedea, 0x2160aca3, 0x93c77766, 0x2d66e105, 0x9ff74d4f, 0x6dc22f21,
-    0x6b03d689, 0x5fc48de0, 0x1138f000, 0xccb58e57, 0xf9c8e200, 0x7ab26e3c, 0xc61dcb3e, 0x6aefccb0,
-    0x7a452f05, 0xa5cf0731, 0xa249383f, 0x628fe534, 0xcad81710, 0x7f616276, 0x3ce18308, 0xed4857ff,
-    0xd1e5b1d1, 0xc2e84dc2, 0xaa003742, 0xaf637488, 0x831afc48, 0x287a69a0, 0x6e04546e, 0x13dffa07,
-    0x3232fb10, 0xd69e2e09, 0x355d8dc7, 0xef902301, 0x9a89ac15, 0x967dc900, 0x08dc2b1c, 0x6b5be690,
-    0x894b0e02, 0xe26af9af, 0xa6fd3b23, 0xfcf213e5, 0x85217608, 0x7fd3be8b, 0xa2e757fb, 0x3717a341,
-    0x85ee426d, 0x394bb856, 0x12ac98c3, 0xec7d4ab5, 0x721b6989, 0x30e36360, 0xaa018403, 0x9ee61196,
-    0xa8697adc, 0x51e9d65a, 0x11023594, 0xc4c4b36b, 0xda80bf7a, 0xbd5a645e, 0x18cea918, 0xa723dda8,
-    0x0126c05e, 0x2962d48a, 0xd5f7d312, 0xb8947041, 0x7c1e2e9a, 0x945eeac3, 0x7110fb1c, 0xa7bc72cc,
-    0xdf47dfbb, 0x09a1c6c8, 0xc2e41061, 0,
+    0x015e7a47, 0x2ef84ebb, 0x177a8db4, 0x1b722ff9, 0x5dc7cff0, 0x5dc9dea6,
+    0x1da0c15a, 0xe4c236a2, 0x3d16b0d0, 0x1f397842, 0xaae0d2ba, 0x11246674,
+    0x0845317f, 0xd5512dad, 0xb6184977, 0xd293a53e, 0x7d9c2716, 0xd917eae6,
+    0xd8852384, 0x286e46f9, 0xce566029, 0xcefe7daf, 0x62d726d4, 0x0dbaeb2d,
+    0x95f57c60, 0xed515141, 0x29b77d0f, 0x9f7b8d0c, 0x45a8395a, 0xfead2b72,
+    0x883d434c, 0xed8ddf60, 0xe51e65e4, 0x19bf6bb1, 0xfeb505ec, 0x662aa23c,
+    0xf6827cf8, 0xd1dc7a5c, 0x4fa5b066, 0x7ddd25a4, 0xa8ba8e8a, 0x72846227,
+    0xf8f636fb, 0x2b389a9c, 0xe4038bf6, 0x6e169877, 0xad028132, 0x84dbfe8c,
+    0x243762ff, 0x59c8f80c, 0xb6e0db4b, 0xedb8cab7, 0xcd4b39f6, 0xaf263741,
+    0x18d9965f, 0x1ab1f037, 0x5b458792, 0xc94d960d, 0xd45cedea, 0x2160aca3,
+    0x93c77766, 0x2d66e105, 0x9ff74d4f, 0x6dc22f21, 0x6b03d689, 0x5fc48de0,
+    0x1138f000, 0xccb58e57, 0xf9c8e200, 0x7ab26e3c, 0xc61dcb3e, 0x6aefccb0,
+    0x7a452f05, 0xa5cf0731, 0xa249383f, 0x628fe534, 0xcad81710, 0x7f616276,
+    0x3ce18308, 0xed4857ff, 0xd1e5b1d1, 0xc2e84dc2, 0xaa003742, 0xaf637488,
+    0x831afc48, 0x287a69a0, 0x6e04546e, 0x13dffa07, 0x3232fb10, 0xd69e2e09,
+    0x355d8dc7, 0xef902301, 0x9a89ac15, 0x967dc900, 0x08dc2b1c, 0x6b5be690,
+    0x894b0e02, 0xe26af9af, 0xa6fd3b23, 0xfcf213e5, 0x85217608, 0x7fd3be8b,
+    0xa2e757fb, 0x3717a341, 0x85ee426d, 0x394bb856, 0x12ac98c3, 0xec7d4ab5,
+    0x721b6989, 0x30e36360, 0xaa018403, 0x9ee61196, 0xa8697adc, 0x51e9d65a,
+    0x11023594, 0xc4c4b36b, 0xda80bf7a, 0xbd5a645e, 0x18cea918, 0xa723dda8,
+    0x0126c05e, 0x2962d48a, 0xd5f7d312, 0xb8947041, 0x7c1e2e9a, 0x945eeac3,
+    0x7110fb1c, 0xa7bc72cc, 0xdf47dfbb, 0x09a1c6c8, 0xc2e41061, 0,
 ];
 
 //# FUNCTION codgen(): UNSIGNED INTEGER;
diff --git a/klee-examples/examples/dwt.rs b/klee-examples/examples/dwt.rs
new file mode 100644
index 0000000000000000000000000000000000000000..210eb7d5cb255328e30c5ff8a5a31ceb53569e77
--- /dev/null
+++ b/klee-examples/examples/dwt.rs
@@ -0,0 +1,27 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate cortex_m;
+
+use core::ptr;
+use cortex_m::peripheral::Peripherals;
+
+#[no_mangle]
+fn main() {
+    let mut 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 {
+        ptr::read_volatile(&dwt);
+    }
+}
diff --git a/klee-examples/examples/path1.rs b/klee-examples/examples/path1.rs
index e6a8334594045413c19bea14a98d692bb3d151e3..c1c85cc8b94095c8f48c3b3f1511ff144f281eb8 100644
--- a/klee-examples/examples/path1.rs
+++ b/klee-examples/examples/path1.rs
@@ -7,13 +7,13 @@ extern crate klee;
 use core::ptr;
 
 #[inline(never)]
-fn add(a:u32, b:u32) -> u32 {
+fn add(a: u32, b: u32) -> u32 {
     a + b
 }
 
 #[no_mangle]
 fn main() {
-    let mut a : [u32; 5] = unsafe { core::mem::uninitialized()};
+    let mut a: [u32; 5] = unsafe { core::mem::uninitialized() };
     // let mut b : [u32; 5] = unsafe { core::mem::uninitialized()};
     ksymbol!(&mut a, "a");
     // ksymbol!(&mut b, "b");
@@ -21,7 +21,7 @@ fn main() {
     for (i, a) in a.iter_mut().enumerate() {
         if *a > 0 {
             *a = a.wrapping_add(1); //  += 1; //  add(*a, 1);
-            // klee::abort();
+                                    // klee::abort();
         }
     }
     // unsafe {