diff --git a/Cargo.toml b/Cargo.toml
index add82fe899e55c2886ee72a05f59c2f83f739a77..3f64f5b9aa6c8e154fd0e0895aa217801741eee2 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -32,7 +32,12 @@ version = "0.2.0"
 
 [features]
 wcet_bkpt = [] 
-wcet_nop = [] 
+wcet_nop = []
+klee = [] 
+
+[profile.dev]
+codegen-units = 1
+incremental = false
 
 [profile.release]
 lto = true
diff --git a/macros/src/check.rs b/macros/src/check.rs
index 3cd112acfd1758d2847365cd91434dd005151d41..9c994a2d62e382bedb9801d9cd5533185b6679b6 100644
--- a/macros/src/check.rs
+++ b/macros/src/check.rs
@@ -6,6 +6,7 @@ use syntax::{self, Resources, Statics};
 
 use syntax::error::*;
 
+#[derive(Debug)]
 pub struct App {
     pub device: Path,
     pub idle: Idle,
@@ -17,6 +18,7 @@ pub struct App {
 pub type Tasks = HashMap<Ident, Task>;
 
 #[allow(non_camel_case_types)]
+#[derive(Debug)]
 pub enum Exception {
     PENDSV,
     SVCALL,
@@ -42,11 +44,13 @@ impl Exception {
     }
 }
 
+#[derive(Debug)]
 pub enum Kind {
     Exception(Exception),
     Interrupt { enabled: bool },
 }
 
+#[derive(Debug)]
 pub struct Task {
     pub kind: Kind,
     pub path: Path,
@@ -63,16 +67,15 @@ pub fn app(app: check::App) -> Result<App> {
         tasks: app.tasks
             .into_iter()
             .map(|(k, v)| {
-                let v = ::check::task(k.as_ref(), v)
-                    .chain_err(|| format!("checking task `{}`", k))?;
+                let v =
+                    ::check::task(k.as_ref(), v).chain_err(|| format!("checking task `{}`", k))?;
 
                 Ok((k, v))
             })
             .collect::<Result<_>>()?,
     };
 
-    ::check::resources(&app)
-        .chain_err(|| "checking `resources`")?;
+    ::check::resources(&app).chain_err(|| "checking `resources`")?;
 
     Ok(app)
 }
diff --git a/macros/src/lib.rs b/macros/src/lib.rs
index bef5dcc1255de8ef47da1ce4736041b691f054bb..eef96b71ae3914bb1ec3ecaf863e221aae1ab3c0 100644
--- a/macros/src/lib.rs
+++ b/macros/src/lib.rs
@@ -181,6 +181,9 @@ fn run(ts: TokenStream) -> Result<TokenStream> {
     let ownerships = analyze::app(&app);
     let tokens = trans::app(&app, &ownerships);
 
+    println!("here we are");
+    println!("{:?}", app.tasks);
+
     Ok(format!("{}", tokens)
         .parse()
         .map_err(|_| "BUG: error parsing the generated code")?)
diff --git a/src/lib.rs b/src/lib.rs
index abc2557aa69c59028f9e3c81991c206568f3d753..0bb4ee95c498aab556be9e163206120c9f17bcad 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -85,6 +85,7 @@ extern crate untagged_option;
 use core::u8;
 
 pub use rtfm_core::{Resource, Static, Threshold};
+#[cfg(not(klee))]
 pub use cortex_m::asm::{bkpt, nop, wfi};
 pub use cortex_m_rtfm_macros::app;
 #[doc(hidden)]
@@ -92,6 +93,7 @@ pub use untagged_option::UntaggedOption;
 
 use cortex_m::interrupt::{self, Nr};
 #[cfg(not(armv6m))]
+#[cfg(not(klee))]
 use cortex_m::register::basepri;
 
 pub mod examples;
@@ -137,17 +139,51 @@ where
                 if ceiling == max_priority {
                     atomic(t, |t| f(data, t))
                 } else {
-                    let old = basepri::read();
+                    let mut old = 0;
+                    // klee mode code generation
+                    // the generated code should not access the hardware
+                    if !cfg!(feature = "klee") {
+                        old = basepri::read();
+                    }
                     let hw = (max_priority - ceiling) << (8 - _nvic_prio_bits);
-                    basepri::write(hw);
-                    if cfg!(feature = "wcet_bkpt") { bkpt(); } 
-                    if cfg!(feature = "wcet_nop") { nop(); }
-                    
+
+                    // klee mode code generation
+                    // the generated code should not access the hardware
+                    if !cfg!(feature = "klee") {
+                        basepri::write(hw);
+                    }
+
+                    // wcet_bkpt mode
+                    // put breakpoint at raise ceiling, for tracing execution time
+                    if cfg!(feature = "wcet_bkpt") {
+                        bkpt();
+                    }
+
+                    // wcet_nop mode
+                    // leave nop in the production code, to keep memory layout the same
+                    if cfg!(feature = "wcet_nop") {
+                        nop();
+                    }
+
                     let ret = f(data, &mut Threshold::new(ceiling));
 
-                    if cfg!(feature = "wcet_bkpt") { bkpt(); } 
-                    if cfg!(feature = "wcet_nop") { nop(); }
-                    basepri::write(old);
+                    // wcet_bkpt mode
+                    // put breakpoint at lower ceiling, for tracing execution time
+                    if cfg!(feature = "wcet_bkpt") {
+                        bkpt();
+                    }
+
+                    // wcet_nop mode
+                    // leave nop in the production code, to keep memory layout the same
+                    if cfg!(feature = "wcet_nop") {
+                        nop();
+                    }
+
+                    // klee mode code generation
+                    // the generated code should not access the hardware
+                    if !cfg!(feature = "klee") {
+                        basepri::write(old);
+                    }
                     ret
                 }
             }