diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
index 6febd18b0ff4190e9fa2b2dc225359e5994e20c3..eb22811726dc92d4b17005994f1f95e481a59f01 100644
--- a/klee-examples/examples/modify.rs
+++ b/klee-examples/examples/modify.rs
@@ -22,6 +22,6 @@ fn main() {
     }
 
     if rw.read() == 0 {
-        klee::abort(); // we directly call the intrinsic abort
+        klee::kabort!(); // we directly call the intrinsic abort
     }
 }
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
index e281cd8d356b8864f3ebb784a2e481fa940bbddd..8d0bc899fc91ec186278a7a641c7eaa279e869d2 100644
--- a/klee-examples/src/peripheral.rs
+++ b/klee-examples/src/peripheral.rs
@@ -18,7 +18,7 @@ fn main() {
     }
     if dwt.ctrl.read() == 0 {
         if dwt.ctrl.read() == 0 {
-            klee::abort();
+            klee::kabort!();
         };
     };
 }
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
index 8024b4efb2051a372e4afcc15bf0db0c789d7098..a5f247c58ec34e6efba8acbded37ca16d2ffbf9e 100644
--- a/klee-examples/src/register.rs
+++ b/klee-examples/src/register.rs
@@ -51,7 +51,7 @@ fn main() {
 
     if rw.read() == 0 {
         if rw.read() == 0 {
-            klee::abort();
+            klee::kabort!();
         }
     }
 }
diff --git a/src/lib.rs b/src/lib.rs
index 2cc7fe10b64536e8b056f0c799ed2d7447a4aa33..91976baa2aa5fc8736904719014af6b595b2b28f 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -16,15 +16,13 @@ use core::ffi::c_void;
 #[doc(hidden)]
 pub use cstr_core::CStr;
 
-#[cfg(feature = "klee-analysis")]
-#[inline(always)]
-pub fn abort() -> ! {
-    unsafe { ll::abort() }
-}
-
-#[cfg(not(feature = "klee-analysis"))]
-pub fn abort() -> ! {
-    panic!(); // leads to the defined panic handler
+/// Aborts the path in KLEE mode, does nothing otherwise
+#[macro_export]
+macro_rules! kabort {
+    () => {
+        #[cfg(feature = "klee-analysis")]
+        unsafe { $crate::ll::abort() };
+    };
 }
 
 #[cfg(feature = "klee-analysis")]
@@ -60,18 +58,16 @@ macro_rules! ksymbol {
     };
 }
 
-#[cfg(feature = "klee-analysis")]
+/// If in KLEE mode, the assertion is made.
+/// Otherwise, this is does nothing.
 #[macro_export]
 macro_rules! kassert {
     ($e:expr) => {
-        if !$e {
-            $crate::abort();
+        #[cfg(feature = "klee-analysis")]
+        {
+            if !$e {
+                $crate::kabort!();
+            }
         }
     };
 }
-
-#[cfg(not(feature = "klee-analysis"))]
-#[macro_export]
-macro_rules! kassert {
-    ($e:expr) => {};
-}