diff --git a/.vscode/tasks.json b/.vscode/tasks.json
index 74b97ef9aadefdee32f89eac357b7b0fbdea4745..15335af1836813e5426c2f387c71e7bf315cec75 100644
--- a/.vscode/tasks.json
+++ b/.vscode/tasks.json
@@ -27,6 +27,18 @@
                 "$rustc"
             ]
         },
+        {
+            "label": "xargo build --example empty2 --features klee_mode --target x86_64-unknown-linux-gnu",
+            "type": "shell",
+            "command": "xargo build --example empty2 --features klee_mode --target x86_64-unknown-linux-gnu",
+            "group": {
+                "kind": "build",
+                "isDefault": true
+            },
+            "problemMatcher": [
+                "$rustc"
+            ]
+        },
         {
             "label": "xargo build --example empty --release --target thumbv7m-none-eabi",
             "type": "shell",
diff --git a/Cargo.toml b/Cargo.toml
index 2b516b78c14da8ba5fba2b25d605ec8361b500ca..3a4cc3b1e737ca9ee083593e79845c1a154af97c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -42,6 +42,7 @@ cm7-r0p1 = ["cortex-m/cm7-r0p1"]
 [profile.dev]
 codegen-units = 1
 incremental = false
+lto = true
 panic = "abort"
 
 [profile.release]
diff --git a/examples/empty2.rs b/examples/empty2.rs
index 42fa9f48d944e955431c552fb3ea7df7a354ad59..97e6be0327e6056e39156ff868a7a67b2b96e6b8 100644
--- a/examples/empty2.rs
+++ b/examples/empty2.rs
@@ -21,20 +21,37 @@ app! {
 }
 
 #[inline(never)]
-fn init(_p: init::Peripherals) {
+fn t() -> i32 {
     let mut x = unsafe { core::mem::uninitialized() };
     let mut y = 0;
     k_symbol!(x, "x");
     if x < 10 {
         for _ in 0..x {
             y += 1;
-            unsafe { core::ptr::read_volatile(&y) };
+            //       unsafe { core::ptr::read_volatile(&y) };
+            //    k_abort();
         }
     }
+    y
+}
 
-    unsafe {
-        k_assert(core::ptr::read_volatile(&y) == 0);
-    }
+#[inline(never)]
+fn init(_p: init::Peripherals) {
+    // let mut x = unsafe { core::mem::uninitialized() };
+    // let mut y = 0;
+    // k_symbol!(x, "x");
+    // if x < 10 {
+    //     for _ in 0..x {
+    //         y += 1;
+    //         unsafe { core::ptr::read_volatile(&y) };
+    //         //    k_abort();
+    //     }
+    // }
+
+    // unsafe {
+    //     k_assert(core::ptr::read_volatile(&y) == 0);
+    // }
+    t();
 }
 
 // The idle loop.