diff --git a/cargo-klee/src/cli.rs b/cargo-klee/src/cli.rs
index b6e9b7f8b40e1980bc8728fccb8cdcddef9d8407..e461c6c3068d8b89084c7bc56ef22b1424da8ade 100644
--- a/cargo-klee/src/cli.rs
+++ b/cargo-klee/src/cli.rs
@@ -31,14 +31,18 @@ pub struct Cli {
     #[arg(long)]
     pub verbose: bool,
 
-    /// Additional arguments to rustc as a string (e.g., "--target", etc)
+    /// Additional arguments to `rustc` as a string (e.g., "--target", etc)
     #[arg(long, allow_hyphen_values = true)]
-    pub rustc: Option<String>,
+    pub rustc_args: Option<String>,
 
     /// Klee invocation
     #[arg(long, short)]
     pub klee: bool,
 
+    /// Additional arguments to `klee` as a string (e.g., "-silent-klee-assume")
+    #[arg(long, allow_hyphen_values = true)]
+    pub klee_args: Option<String>,
+
     /// GDB Replay
     #[arg(long, short)]
     pub replay: bool,
@@ -102,9 +106,32 @@ fn cli_parse_bin_all_features() {
 }
 
 #[test]
-fn cli_parse_bin_rustc() {
-    let args = Cli::try_parse_from(&["test", "klee", "--rustc", "--target=wasm32-unknown-unknown"])
-        .unwrap();
+fn cli_parse_bin_rustc_args() {
+    let args = Cli::try_parse_from(&[
+        "test",
+        "klee",
+        "--rustc-args",
+        "--target=wasm32-unknown-unknown",
+    ])
+    .unwrap();
+    println!("args {:?}", args);
+    assert_eq!(&args.rustc_args.unwrap(), "--target=wasm32-unknown-unknown");
+}
+
+#[test]
+fn cli_parse_bin_klee_args() {
+    let args =
+        Cli::try_parse_from(&["test", "klee", "--klee-args", "-silent-klee-assume"]).unwrap();
+    println!("args {:?}", args);
+    assert_eq!(&args.klee_args.unwrap(), "-silent-klee-assume");
+}
+
+#[test]
+fn cli_parse_bin_klee_args2() {
+    let args = Cli::try_parse_from(&["test", "klee", "--klee-args", "-foo -bar"]).unwrap();
     println!("args {:?}", args);
-    assert_eq!(&args.rustc.unwrap(), "--target=wasm32-unknown-unknown");
+    let klee_args = args.klee_args.unwrap();
+    let vec: Vec<&str> = klee_args.split(" ").collect();
+    println!("vec {:?}", vec);
+    assert_eq!(vec, vec!["-foo", "-bar"]);
 }
diff --git a/cargo-klee/src/main.rs b/cargo-klee/src/main.rs
index 5addb95f68b642a33aac00530e3a2a4f6524650d..db6535fc8fac0bec4d02d2286581ad389c1767f3 100644
--- a/cargo-klee/src/main.rs
+++ b/cargo-klee/src/main.rs
@@ -1,44 +1,21 @@
 use anyhow::{anyhow, Error};
 
 // use std::error::Error;
-use cargo_klee::cli::Cli;
+use cargo_klee::{
+    cargo_out::{get_hash, get_out_dir},
+    cli::Cli,
+};
 use clap::Parser;
-use std::str::Split;
-
-// extern crate libc;
-
 use std::{
-    env, fs,
-    path::PathBuf,
-    process::{self, Command, ExitStatus, Stdio},
-    time::SystemTime,
+    env,
+    process::{Command, Stdio},
+    str::Split,
 };
 
-use cargo_project::{Artifact, Profile, Project};
-
-// #[derive(Debug, Parser)]
-// #[command(author, version, about, long_about = None)]
-// struct Cli {
-//     /// Fields to use as part of the line's key
-//     #[clap(long, short)]
-//     fields: FieldSpec,
-// }
-
-// #[derive(Debug, Clone)]
-// struct FieldSpec {
-//     indices: Vec<usize>,
-// }
+// extern crate libc;
 
-// impl std::str::FromStr for FieldSpec {
-//     type Err = Error;
-//     fn from_str(s: &str) -> Result<Self, Self::Err> {
-//         let mut indices = Vec::new();
-//         for f in s.split(',') {
-//             indices.push(usize::from_str(f)?);
-//         }
-//         Ok(FieldSpec { indices })
-//     }
-// }
+// use cargo_project::{Artifact, Profile,  Project};
+use cargo_project::Project;
 
 fn main() -> Result<(), Error> {
     let args = Cli::try_parse()?;
@@ -85,13 +62,14 @@ fn main() -> Result<(), Error> {
         }
     }
 
+    // propagate release flag
     if args.release {
         cargo.arg("--release");
     }
+
     // propagate additional arguments to rustc, e.g. --target=wasm32-unknown-unknown
-    // TODO! this is not tested
-    if let Some(rustc) = args.rustc {
-        let vec: Vec<&str> = rustc.split(" ").collect();
+    if let Some(args) = args.rustc_args {
+        let vec: Vec<&str> = args.split(" ").collect();
         for v in vec {
             cargo.arg(v);
         }
@@ -126,15 +104,6 @@ fn main() -> Result<(), Error> {
         eprintln!("\n{:?}\n", cargo);
     }
 
-    // // execute the command and unwrap the result into status
-    // let status = cargo.status()?;
-
-    // if !status.success() {
-    //     // TODO! correctly handle exit status
-    //     panic!("{:?}", status);
-    //     // return Err(status.code().unwrap_or(1).into());
-    // }
-
     println!("project name {:?}", project.name());
     println!("project target {:?}", project.target());
     println!("project toml {:?}", project.toml());
@@ -143,21 +112,77 @@ fn main() -> Result<(), Error> {
     let output = cargo.stdout(Stdio::piped()).output()?;
     let stderr = String::from_utf8(output.stderr)?;
 
-    // We enforce color, assumes standard utf-8 coding for Green
+    // We enforce color, assumes standard utf-8 coding for Green "Compiling"
     let comp = "\u{1b}[32m   Compiling";
-    let s: Split<&str> = stderr.split(comp);
-    let last = s.last().unwrap();
+    let split: Split<&str> = stderr.split(comp);
+    let last = split
+        .last()
+        .expect("failed to capture `cargo Compiling` output");
 
+    // Print output to stderr, from `cargo` to user.
     if args.verbose {
-        println!("{}", stderr);
+        eprintln!("{}", stderr);
     } else {
-        println!("{}{}", comp, last);
+        eprintln!("{}{}", comp, last);
     }
 
     if !output.status.success() {
-        return Err(anyhow!("Compilation failed, exiting cargo-klee"));
+        return Err(anyhow!("Compilation failed, exiting `cargo-klee`"));
     }
 
+    let out_dir = get_out_dir(last).expect("failed to locate --out-dir");
+    let hash = get_hash(last).expect("failed to locate -C metadata");
+
+    println!("out_dir {}", out_dir);
+    println!("hash {}", hash);
+
+    let ll = format!("{}/{}-{}.ll", out_dir, file, hash);
+    println!("ll {}", ll);
+
+    // KLEE analysis
+    if args.klee {
+        println!("--- klee-analysis ---\n");
+        let mut klee = Command::new("klee");
+
+        // propagate additional arguments to klee, e.g. "-silent-klee-assume"
+        if let Some(args) = args.klee_args {
+            let vec: Vec<&str> = args.split(" ").collect();
+            for v in vec {
+                klee.arg(v);
+            }
+        }
+        // --disable-very to suppress know issue in klee https://github.com/klee/klee/issues/937
+        klee.arg("--disable-verify")
+            // enable coloring of output
+            .arg("--color")
+            // ll file to analyse
+            .arg(ll);
+
+        println!("klee {:?}", klee);
+
+        // For some reason capturing output does not work with colors.
+        // let output = klee.stdout(Stdio::piped()).output()?;
+        // let stderr = String::from_utf8(output.stderr)?;
+        // eprintln!("{}", stderr);
+
+        // Workaround using `.status` to propagate `klee` output to `stderr`.
+        let output = klee
+            .stdout(Stdio::piped())
+            .status()
+            .expect("failed to invoke `klee`, exiting `cargo-klee`");
+
+        if !output.success() {
+            return Err(anyhow!("`klee` failed, exiting `cargo-klee`"));
+        }
+
+        let output = klee.stdout(Stdio::piped()).output()?;
+        let stderr = String::from_utf8(output.stderr)?;
+
+        eprintln!("{}", stderr);
+    }
+
+    println!("--- done ---");
+
     Ok(())
 }