diff --git a/.cargo/config b/.cargo/config
index 901b89afec3a9bedf3243265e536b4c3673315e8..f84ab0120ef0fa89cf7d07d02a2df647a7d9139c 100644
--- a/.cargo/config
+++ b/.cargo/config
@@ -28,6 +28,7 @@ rustflags = [
   "-C", "link-arg=-Tlink.x",
   "-C", "linker=arm-none-eabi-ld",
   "-Z", "linker-flavor=ld",
+  "-Z", "thinlto=no",
 ]
 
 # used when building for klee
@@ -35,7 +36,8 @@ rustflags = [
 [target.x86_64-unknown-linux-gnu]
 rustflags = [
   "--emit=llvm-bc,llvm-ir",
-  "-C", "linker=true"
+  "-C", "linker=true",
+  "-Z", "thinlto=no",
 ]
 
 # default build target (for m3)
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index 31b22b5a9e06768687b0431e00d2926a42a1e730..52044219ae206d843aec228f9537609a08c9a2a5 100644
--- a/klee/src/lib.rs
+++ b/klee/src/lib.rs
@@ -7,7 +7,7 @@ extern crate cstr_core;
 extern crate cty;
 
 // mod lang_items;
-mod ll;
+pub mod ll;
 
 use core::mem;
 
@@ -42,7 +42,7 @@ pub fn k_mk_symbol<T>(t: &mut T, name: &CStr) {
     }
 }
 
-#[inline(never)]
+#[inline(always)]
 pub fn k_abort() -> ! {
     unsafe {
         ll::abort();
@@ -50,7 +50,7 @@ pub fn k_abort() -> ! {
 }
 
 /// assume a condition involving symbolic variables
-#[inline(never)]
+#[inline(always)]
 pub fn k_assume(cond: bool) {
     unsafe {
         ll::klee_assume(cond);
@@ -58,10 +58,12 @@ pub fn k_assume(cond: bool) {
 }
 
 /// assert a condition involving symbolic variables
-#[inline(never)]
+#[inline(always)]
 pub fn k_assert(e: bool) {
     if !e {
-        k_abort();
+        unsafe {
+            ll::abort();
+        }
     }
 }
 
@@ -70,12 +72,27 @@ pub fn k_assert(e: bool) {
 macro_rules! k_symbol {
     ($id:expr, $name:expr) => {
         {
-        #[allow(unsafe_code)]
-        #[allow(warnings)]
-        $crate::k_mk_symbol(
-            unsafe { $id },
-            unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
-        )
+            #[allow(unsafe_code)]
+            #[allow(warnings)]
+            $crate::k_mk_symbol(
+                unsafe { $id },
+                unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
+            )
+        }
+    }
+}
+
+/// assertion
+#[macro_export]
+macro_rules! k_assert {
+    ($e: expr) => {
+        {
+            use klee::ll;
+            if !$e {
+                unsafe {
+                    ll::abort();
+                }
+            }
         }
     }
 }
diff --git a/klee/src/ll.rs b/klee/src/ll.rs
index d8144103613ebc629feecc868775251ad3488928..01d25d5f33a43297a9f9713ecf550ca79cda6658 100644
--- a/klee/src/ll.rs
+++ b/klee/src/ll.rs
@@ -8,12 +8,15 @@ extern "C" {
 }
 
 #[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
 pub unsafe fn abort() -> ! {
     loop {}
 }
 
 #[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
 pub unsafe fn klee_assume(_cond: bool) {}
 
 #[cfg(not(feature = "klee_mode"))]
+#[inline(always)]
 pub unsafe fn klee_make_symbolic(_ptr: *mut c_void, _size: usize, _name: *const c_char) {}