diff --git a/README.md b/README.md
index e479a867c730f4924e734bbdb5ad13749170aa41..7ea386af312dcfb89741f48c45b84b5ea3fd88a9 100644
--- a/README.md
+++ b/README.md
@@ -8,31 +8,42 @@ LLVM KLEE performs symbolic execution of LLVM-IR programs. For each path KLEE wi
 
 A path is termintated either by executing to end or hitting the `abort` symbol. We bind the Rust `panic_handler` to the `abort` symbol, thus any `panic!()` will result in path termination (and consequitively a concrete test).
 
-As `assert!()`/`assert_eq!()` etc. expands to conditional `panic!()`, any failing assertion will generate a concrete test.
+As `assert!()`/`assert_eq!()` etc. expands to conditional `panic!()`, thus a failing assertion will be caught.
 
-Variables (or rather memory locations) can be made symbolic, through the C API.
+Variables (or rather `memory objects`) can be made symbolic, through the KLEE C API. We bind the KLEE API in the `ll` module.
 
 ``` Rust
 pub fn klee_make_symbolic(
-    ptr: *mut core::ffi::c_void,    // pointer do the data 
-    size: usize,                    // size (in bytes)
-    name: *const i8                 // pointer to zero-teriminted C string
-);
+        ptr: *mut core::ffi::c_void,    // pointer to the data
+        size: usize,                    // size (in bytes)
+        name: *const cstr_core::c_char, // pointer to zero-terminted C string
+    );
+}
 ```
 
-The internal Rust abstraction:
+The internal Rust abstraction, calls into the FFI binding.
 
 ``` Rust
 fn klee_make_symbolic<T>(
     t: &mut T,                      // reference to generic type
-    name: &'static CStr             // pointer to CString 
+    name: &'static CStr             // reference to static CStr
 ) {...}
 ```
 
-However dealing with CStr is cumbersome in user code so we provide a macro, `klee_mk_symbol!(&mut T, &str)`, that zero-termintes the `&str`. You can use
+However dealing with CStr is cumbersome in Rust user code so we provide a macro, `klee_make_symbolic!(&mut T, &str)`, that zero-termintes the `&str` and cast it to the appropriate type.
+
+Example usage:
 
 ``` Rust
     ...
     let mut a = 0;
     klee_make_symbolic(&mut a, "a");
 ```
+
+## KLEE test case generation
+
+LLVM KLEE strives to cover all feasible paths. When generating tests for errors encountered (paths to `abort`), KLEE will generate *one* test for each unique position in the source code that lead up to the `abort`. Code that emits a Rust `panic!()`, will all reach the same `panic_handler` (which calls into `abort`), and KLEE will detect the `panic_handler` as the source of the error, and consequently generate *one* such test. (Perhaps there is a way to force KLEE to generate one test per unique path leading up to the `panic_handler`, but we have not yet found it. Tech note: The `panic` implementation can unfortunately not be inlined as far as we have seen.)
+
+As a consequence, you have to eleminate sources of `panic!()` one by one, which may be time consuming.
+
+We provide a set of macros `klee_abort`, `klee_assert` and `klee_assert_eq`, that gets fully inlined, allowing KLEE to generate specific tests for each failing assertion.
diff --git a/src/lib.rs b/src/lib.rs
index cdbb617cde7ea097ebea62b819b6d0409112ac2d..6528a38f75f3136ffede4770d5b615c4ae1747d9 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,6 +1,8 @@
 #![no_std]
 
 use core::ffi::c_void;
+use cstr_core::c_char;
+
 #[doc(hidden)]
 pub use cstr_core::CStr;
 
@@ -8,8 +10,7 @@ pub mod ll;
 
 pub mod panic;
 
-//#[inline(always)]
-#[inline(never)]
+#[inline(always)]
 pub fn klee_abort() -> ! {
     unsafe { ll::abort() };
 }
@@ -21,24 +22,42 @@ pub fn klee_assume(cond: bool) {
     }
 }
 
-// #[inline(always)]
-// pub fn klee_assert(cond: bool) {
-//     if !cond {
-//         klee_abort();
-//     }
-// }
-
 #[inline(always)]
-fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
+pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
     unsafe {
         ll::klee_make_symbolic(
             t as *mut T as *mut c_void,
             core::mem::size_of::<T>(),
-            name.as_ptr() as *const u8,
+            name.as_ptr() as *const c_char,
         )
     }
 }
 
+#[macro_export]
+macro_rules! klee_abort {
+    () => {
+        unsafe { $crate::ll::abort() };
+    };
+}
+
+#[macro_export]
+macro_rules! klee_assert {
+    ($e:expr) => {{
+        if !$e {
+            unsafe { $crate::ll::abort() };
+        }
+    }};
+}
+
+#[macro_export]
+macro_rules! klee_assert_eq {
+    ($e1:expr, $e2:expr ) => {{
+        if !($e1 == $e2) {
+            unsafe { $crate::ll::abort() };
+        }
+    }};
+}
+
 #[macro_export]
 macro_rules! klee_make_symbolic {
     (&mut $id:expr, $name:expr) => {
diff --git a/src/ll.rs b/src/ll.rs
index 98cadac3449006cbbb7fccdff1eef709360d0dc6..2010aebf357997496f0e6202ebbcc84a109b0331 100644
--- a/src/ll.rs
+++ b/src/ll.rs
@@ -1,8 +1,9 @@
 extern "C" {
-    #[inline(always)]
     pub fn abort() -> !;
-    #[inline(always)]
     pub fn klee_assume(cond: bool);
-    #[inline(always)]
-    pub fn klee_make_symbolic(ptr: *mut core::ffi::c_void, size: usize, name: *const u8);
+    pub fn klee_make_symbolic(
+        ptr: *mut core::ffi::c_void,    // pointer to the data
+        size: usize,                    // size (in bytes)
+        name: *const cstr_core::c_char, // pointer to zero-terminted C string
+    );
 }
diff --git a/src/panic.rs b/src/panic.rs
index a910203ce8a66911b73cd40a91cdc2acf4c2b578..f3d1fc345d754401478a5615ded33969d4a6270e 100644
--- a/src/panic.rs
+++ b/src/panic.rs
@@ -1,6 +1,5 @@
 #[cfg(not(test))] // avoid warning duplicate lang-item
 #[panic_handler]
-#[inline(never)]
 fn panic(_info: &core::panic::PanicInfo) -> ! {
     // abort symbol caught by LLVM-KLEE
     unsafe { crate::ll::abort() }