diff --git a/.vscode/settings.json b/.vscode/settings.json
index 0aa00e41b16cbadb7490e3946f925bb52dc6eeb3..9df12806128d657acb065e025b7fefd33f0da02c 100644
--- a/.vscode/settings.json
+++ b/.vscode/settings.json
@@ -1,6 +1,7 @@
 {
     "cSpell.ignoreWords": [
         "Runtest",
+        "analyse",
         "deps",
         "is",
         "istats",
diff --git a/README.md b/README.md
index b921ebfa5485883d5ee09bc2b17ac2253b5189de..2829a62130b6e3dd86c2aef17feff084120e346a 100644
--- a/README.md
+++ b/README.md
@@ -8,12 +8,12 @@ In effect, a Rust program passing KLEE analysis is thus ensured to be panic free
 
 ## Requirements
 
-- LLVM KLEE installed, (version 2.3pre, currently based on LLVM-v12).
-- LLVM llc and clang for building replay binaries (currently based on LLVM-v12).
-- GNU gdb for executing replay binaries
-- Rust tool-chain (edition-2018), tested with stable `rustc 1.56.1 (59eed8a2a 2021-11-01)`.
+- LLVM KLEE installed, (tested under arch linux 220929 with version 2.3 on LLVM-v14).
+- LLVM llc and clang for building replay binaries (currently based on LLVM-v14).
+- GNU gdb for executing replay binaries.
+- Rust tool-chain (edition-2018), tested with stable `rustc 1.64.0 (a55dd71d5 2022-09-19)`.
   
-The `klee` tools (executables) needs to be installed and accessible in path, the KLEE libraries are assumed to be accessible under `/usr/lib`. The tool has been tested on the master branch of [KLEE](https://github.com/klee/klee) 2.3pre as of 2021-11-04, built under arch linux with the system LLVM (v12). You may use a custom install of KLEE, set the `LD_LIBRARY_PATH` to include the location of `kleeRuntest.so.1.0` (used by cargo-klee to dynamically link the library for replay of tests in gdb).
+The `klee` tools (executables) needs to be installed and accessible in path, the KLEE libraries are assumed to be accessible under `/usr/lib`. The tool has been tested on the master branch of [KLEE](https://github.com/klee/klee) 2.3 as of 2022-09-29, built under arch linux with the system LLVM (v14). You may use a custom install of KLEE, set the `LD_LIBRARY_PATH` to include the location of `kleeRuntest.so.1.0` (used by cargo-klee to dynamically link the library for replay of tests in gdb).
 
 ## Limitations
 
diff --git a/cargo-klee/.vscode/settings.json b/cargo-klee/.vscode/settings.json
new file mode 100644
index 0000000000000000000000000000000000000000..8b594332075e0be62dbe6efdd535df0752280a6e
--- /dev/null
+++ b/cargo-klee/.vscode/settings.json
@@ -0,0 +1,6 @@
+{
+    "cSpell.ignoreWords": [
+        "LuleƄ",
+        "rustc"
+    ]
+}
\ No newline at end of file
diff --git a/cargo-klee/Cargo.toml b/cargo-klee/Cargo.toml
index 95832a2c69f48fc9ab4a11ed956a23350c47abe2..8614ece38ad84a7ee7ead29c0dae619e8a49459d 100644
--- a/cargo-klee/Cargo.toml
+++ b/cargo-klee/Cargo.toml
@@ -1,13 +1,17 @@
 [package]
 authors = ["Lulea University of Technology (LTU)"]
 name = "cargo-klee"
-version = "0.4.0"
-edition = "2018"
+about = "KLEE analysis of Rust application"
+long_about = "Cargo sub-command to manage building a Rust application for KLEE analysis, running KLEE analysis and replaying generated tests using `gdb`"
+
+version = "0.5.0"
+edition = "2021"
 
 [dependencies]
 libc = "0.2.81"
-failure = "0.1.8"
-cargo-project = "0.2.4"
+# failure = "0.1.8"
+cargo-project = "0.3.0"
 either = "1.6.1"
-clap = "2.33.3"
-rustc_version = "0.3.0"
+clap = { version = "4.0.6", features = ["derive", "color"] }
+rustc_version = "0.4.0"
+anyhow = "1.0.65"
diff --git a/cargo-klee/src/cli.rs b/cargo-klee/src/cli.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6052692ef795c003b776bf12a3a031d5491f18b9
--- /dev/null
+++ b/cargo-klee/src/cli.rs
@@ -0,0 +1,68 @@
+// use anyhow::Error;
+// use clap::{Arg, ArgGroup, Parser, Subcommand};
+use clap::{ArgGroup, Parser};
+#[derive(Parser, Debug, Clone)] // requires `derive` feature
+#[command(author, version, about, long_about = None)]
+#[command(group(ArgGroup::new("binary").multiple(false)))]
+pub struct Cli {
+    // klee argument passed implicitly by Cargo
+    command: String,
+    /// Binary to build
+    #[arg(long, group = "binary")]
+    bin: Option<String>,
+
+    /// Example to build
+    #[arg(long, group = "binary")]
+    example: Option<String>,
+
+    /// Arguments to rustc as a string (e.g., "--release, --target", etc)
+    #[arg(long, allow_hyphen_values = true)]
+    rustc: Option<String>,
+
+    /// Verbose output from rustc
+    #[arg(long)]
+    verbose: bool,
+
+    /// Klee invocation
+    #[arg(long, short)]
+    klee: bool,
+
+    /// GDB Replay
+    #[arg(long, short)]
+    replay: bool,
+    // #[command(subcommand)]
+    // binary: Option<Commands>,
+}
+
+#[test]
+fn cli_verify() {
+    use clap::CommandFactory;
+    Cli::command().debug_assert()
+}
+
+#[test]
+fn cli_parse_simple() {
+    let args = Cli::try_parse_from(&["test"]).unwrap();
+    assert_eq!(args.bin, None);
+}
+
+#[test]
+fn cli_parse_bin() {
+    let args = Cli::try_parse_from(&["test", "klee", "--bin", "a"]).unwrap();
+    println!("args {:?}", args);
+    assert_eq!(args.bin, Some("a".to_owned()));
+}
+
+#[test]
+fn cli_parse_example() {
+    let args = Cli::try_parse_from(&["test", "klee", "--example", "b"]).unwrap();
+    println!("args {:?}", args);
+    assert_eq!(args.example, Some("b".to_owned()));
+}
+
+#[test]
+fn cli_parse_bin_example() {
+    let args = Cli::try_parse_from(&["test", "klee", "--bin", "a", "--example", "b"]);
+    println!("args {:?}", args);
+    assert_eq!(args.is_err(), true);
+}
diff --git a/cargo-klee/src/lib.rs b/cargo-klee/src/lib.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4f773726a20b821d11320ef75d522be0bc862871
--- /dev/null
+++ b/cargo-klee/src/lib.rs
@@ -0,0 +1 @@
+pub mod cli;
diff --git a/cargo-klee/src/main.rs b/cargo-klee/src/main.rs
index 002d7209896562be5f014d5ab58bf94c974e21ea..852abb011b5adb9847870fcb956693dc1240f665 100644
--- a/cargo-klee/src/main.rs
+++ b/cargo-klee/src/main.rs
@@ -1,321 +1,365 @@
-extern crate libc;
-
-use std::{
-    env, fs,
-    path::PathBuf,
-    process::{self, Command},
-    time::SystemTime,
-};
-
-use cargo_project::{Artifact, Profile, Project};
-use clap::{App, Arg};
-
-fn main() -> Result<(), failure::Error> {
-    match run() {
-        Ok(ec) => process::exit(ec),
-        Err(e) => {
-            eprintln!("error: {}", e);
-            process::exit(1)
-        }
-    }
+use anyhow::Error;
+
+// use std::error::Error;
+use cargo_klee::cli::Cli;
+use clap::Parser;
+
+// extern crate libc;
+
+// use std::{
+//     env, fs,
+//     path::PathBuf,
+//     process::{self, Command},
+//     time::SystemTime,
+// };
+
+// 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>,
+// }
+
+// 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 })
+//     }
+// }
+
+fn main() -> Result<(), Error> {
+    let args = Cli::parse();
+
+    println!("{:?}", args);
+    Ok(())
 }
 
-fn run() -> Result<i32, failure::Error> {
-    let matches = App::new("cargo-klee")
-        .version("0.4.0")
-        .author("Lulea University of Technology (LTU)")
-        .about("KLEE analysis of Rust application")
-        // as this is used as a Cargo sub-command the first argument will be the name of the binary
-        // we ignore this argument
-        .arg(Arg::with_name("binary-name").hidden(true))
-        // TODO: custom target support (for now only target host is supported)
-        // .arg(
-        //     Arg::with_name("target")
-        //         .long("target")
-        //         .takes_value(true)
-        //         .value_name("TRIPLE")
-        //         .help("Target triple for which the code is compiled"),
-        // )
-        .arg(
-            Arg::with_name("verbose")
-                .long("verbose")
-                .short("v")
-                .help("Use verbose output"),
-        )
-        .arg(
-            Arg::with_name("example")
-                .long("example")
-                .takes_value(true)
-                .value_name("NAME")
-                .required_unless("bin")
-                .conflicts_with("bin")
-                .help("Build only the specified example"),
-        )
-        .arg(
-            Arg::with_name("bin")
-                .long("bin")
-                .takes_value(true)
-                .value_name("NAME")
-                .required_unless("example")
-                .conflicts_with("example")
-                .help("Build only the specified binary"),
-        )
-        .arg(
-            Arg::with_name("release")
-                .long("release")
-                .help("Build artifacts in release mode, with optimizations"),
-        )
-        .arg(
-            Arg::with_name("features")
-                .long("features")
-                .takes_value(true)
-                .value_name("FEATURES")
-                .help("Space-separated list of features to activate"),
-        )
-        .arg(
-            Arg::with_name("all-features")
-                .long("all-features")
-                .takes_value(false)
-                .help("Activate all available features"),
-        )
-        // TODO, support additional parameters to KLEE
-        .arg(
-            Arg::with_name("klee")
-                .long("klee")
-                .short("k")
-                .help("Run KLEE test generation [default enabled unless --replay]"),
-        )
-        .arg(
-            Arg::with_name("replay")
-                .long("replay")
-                .short("r")
-                .help("Generate replay binary in target directory"),
-        )
-        .arg(
-            Arg::with_name("gdb")
-                .long("gdb")
-                .short("g")
-                .help("Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the `gdb` working directory, if unset `gdb` will execute in the current working directory"),
-        )
-        .get_matches();
-
-    let is_example = matches.is_present("example");
-    let is_binary = matches.is_present("bin");
-    let verbose = matches.is_present("verbose");
-    let is_release = matches.is_present("release");
-    let is_replay = matches.is_present("replay");
-    let is_ktest = matches.is_present("klee");
-    let is_gdb = matches.is_present("gdb");
-
-    // let target_flag = matches.value_of("target"); // not currently supported
-
-    // we rely on `clap` for either `example` or `bin`
-    let file = if is_example {
-        matches.value_of("example").unwrap()
-    } else {
-        matches.value_of("bin").unwrap()
-    };
-
-    // turn `cargo klee --example foo` into `cargo rustc --example foo -- (..)`
-    let mut cargo = Command::new("cargo");
-    cargo
-        // compile using rustc
-        .arg("rustc")
-        // verbose output for debugging purposes
-        .arg("-v");
-
-    // set features, always including `klee-analysis`
-    if matches.is_present("all-features") {
-        cargo.arg("--all-features");
-    } else {
-        if let Some(features) = matches.value_of("features") {
-            let mut vec: Vec<&str> = features.split(" ").collect::<Vec<&str>>();
-            vec.push("klee-analysis");
-            cargo.args(&["--features", &vec.join(" ")]);
-        } else {
-            cargo.args(&["--features", "klee-analysis"]);
-        }
-    }
-
-    // select (single) application to compile
-    // derive basic settings from `cargo`
-    if is_example {
-        cargo.args(&["--example", file]);
-    } else {
-        cargo.args(&["--bin", file]);
-    }
-
-    // default is debug mode
-    if is_release {
-        cargo.arg("--release");
-    }
-
-    cargo
-        // enable shell coloring of result
-        .arg("--color=always")
-        .arg("--")
-        // ignore linking
-        .args(&["-C", "linker=true"])
-        // force LTO, to get a single oject file
-        .args(&["-C", "lto"])
-        // output the LLVM-IR (.ll file) for KLEE analysis
-        .arg("--emit=llvm-ir")
-        // force panic=abort in all crates, override .cargo settings
-        .env("RUSTFLAGS", "-C panic=abort");
-    // TODO, force `incremental=false`, `codegen-units=1`?
-
-    if verbose {
-        eprintln!("\n{:?}\n", cargo);
-    }
-
-    // execute the command and unwrap the result into status
-    let status = cargo.status()?;
-
-    if !status.success() {
-        return Ok(status.code().unwrap_or(1));
-    }
-
-    let cwd = env::current_dir()?;
-
-    let meta = rustc_version::version_meta()?;
-    let host = meta.host;
-
-    let project = Project::query(cwd)?;
-
-    let profile = if is_release {
-        Profile::Release
-    } else {
-        Profile::Dev
-    };
-
-    let mut path: PathBuf = if is_example {
-        project.path(Artifact::Example(file), profile, None, &host)?
-    } else {
-        project.path(Artifact::Bin(file), profile, None, &host)?
-    };
-
-    // llvm-ir file
-    let mut ll = None;
-    // most recently modified
-    let mut mrm = SystemTime::UNIX_EPOCH;
-    let prefix = format!("{}-", file.replace('-', "_"));
-
-    path = path.parent().expect("unreachable").to_path_buf();
-
-    if is_binary {
-        path = path.join("deps"); // the .ll file is placed in ../deps
-    }
-
-    // lookup the latest .ll file
-    // TODO: stable support for `metadata` from Cargo.
-    for e in fs::read_dir(path)? {
-        let e = e?;
-        let p = e.path();
-
-        if p.extension().map(|e| e == "ll").unwrap_or(false) {
-            if p.file_stem()
-                .expect("unreachable")
-                .to_str()
-                .expect("unreachable")
-                .starts_with(&prefix)
-            {
-                let modified = e.metadata()?.modified()?;
-                if ll.is_none() {
-                    ll = Some(p);
-                    mrm = modified;
-                } else {
-                    if modified > mrm {
-                        ll = Some(p);
-                        mrm = modified;
-                    }
-                }
-            }
-        }
-    }
-
-    let mut obj = ll.clone().unwrap();
-    let replay_name = obj.with_file_name(file).with_extension("replay");
-
-    // replay compilation
-    if is_replay {
-        // compile to object code for replay using `llc`
-        let mut llc = Command::new("llc");
-        llc.arg("-filetype=obj")
-            .arg("-relocation-model=pic")
-            .arg(ll.clone().unwrap());
-
-        if verbose {
-            eprintln!("\n{:?}\n", llc);
-        }
-
-        // TODO: better error handling, e.g., if `llc` is not installed/in path
-        let status = llc.status()?;
-        if !status.success() {
-            println!("llc failed: {:?}", status.code().unwrap_or(1));
-        } else {
-            // compile to executable for replay using `clang`
-            let mut clang = Command::new("clang");
-
-            obj = obj.with_extension("o");
-
-            clang
-                .arg(obj)
-                .arg("--rtlib=compiler-rt")
-                .arg("-lkleeRuntest")
-                .args(&["-o", replay_name.to_str().unwrap()]);
-
-            if verbose {
-                eprintln!("\n{:?}\n", clang);
-            }
-
-            // TODO: better error handling, e.g., if `clang` in not installed/in path
-            let status = clang.status()?;
-            if !status.success() {
-                println!("clang failed: {:?}", status.code().unwrap_or(1));
-            }
-        }
-    }
-
-    // klee analysis
-    if is_ktest || !is_replay {
-        let mut klee = Command::new("klee");
-        // --disable-very to suppress know issue in klee https://github.com/klee/klee/issues/937
-        klee.arg("--disable-verify")
-            // ll file to analyse
-            .arg(ll.unwrap());
-
-        // execute the command and unwrap the result into status
-        let status = klee.status()?;
-        if !status.success() {
-            return Ok(status.code().unwrap_or(1));
-        }
-    }
-
-    // replay execution in `gdb`
-    if is_gdb {
-        let mut gdb = Command::new("gdb");
-        if let Ok(cwd) = env::var("GDB_CWD") {
-            // set gdb current dir to `GDB_CWD`
-            gdb.current_dir(cwd);
-            // set replay name to be loaded by `gdb`
-            gdb.arg(replay_name);
-        } else {
-            // set gdb current dir to the target directory
-            gdb.current_dir(replay_name.parent().unwrap());
-            // set replay name to be loaded by gdb
-            gdb.arg(replay_name.file_name().unwrap());
-        };
-
-        if verbose {
-            eprintln!("\n{:?}\n", gdb);
-        }
-
-        // TODO: better error handling, e.g., if `gdb` is not installed/in path
-        let status = gdb.status()?;
-        if !status.success() {
-            println!("gdb failed: {:?}", status.code().unwrap_or(1));
-        }
-    }
-    // return to shell without error
-    Ok(0)
-}
+// fn main() -> Result<(), Box<dyn std::error::Error>> {
+//     let args = Cli::parse();
+//     println!("args {:?}", args);
+//     Ok(())
+// }
+// fn main() -> Result<(), failure::Error> {
+//     match run() {
+//         Ok(ec) => process::exit(ec),
+//         Err(e) => {
+//             eprintln!("error: {}", e);
+//             process::exit(1)
+//         }
+//     }
+// }
+
+// fn run() -> Result<i32, failure::Error> {
+//     let matches = App::new("cargo-klee")
+//         .version("0.4.0")
+//         .author("Lulea University of Technology (LTU)")
+//         .about("KLEE analysis of Rust application")
+//         // as this is used as a Cargo sub-command the first argument will be the name of the binary
+//         // we ignore this argument
+//         .arg(Arg::with_name("binary-name").hidden(true))
+//         // TODO: custom target support (for now only target host is supported)
+//         // .arg(
+//         //     Arg::with_name("target")
+//         //         .long("target")
+//         //         .takes_value(true)
+//         //         .value_name("TRIPLE")
+//         //         .help("Target triple for which the code is compiled"),
+//         // )
+//         .arg(
+//             Arg::with_name("verbose")
+//                 .long("verbose")
+//                 .short("v")
+//                 .help("Use verbose output"),
+//         )
+//         .arg(
+//             Arg::with_name("example")
+//                 .long("example")
+//                 .takes_value(true)
+//                 .value_name("NAME")
+//                 .required_unless("bin")
+//                 .conflicts_with("bin")
+//                 .help("Build only the specified example"),
+//         )
+//         .arg(
+//             Arg::with_name("bin")
+//                 .long("bin")
+//                 .takes_value(true)
+//                 .value_name("NAME")
+//                 .required_unless("example")
+//                 .conflicts_with("example")
+//                 .help("Build only the specified binary"),
+//         )
+//         .arg(
+//             Arg::with_name("release")
+//                 .long("release")
+//                 .help("Build artifacts in release mode, with optimizations"),
+//         )
+//         .arg(
+//             Arg::with_name("features")
+//                 .long("features")
+//                 .takes_value(true)
+//                 .value_name("FEATURES")
+//                 .help("Space-separated list of features to activate"),
+//         )
+//         .arg(
+//             Arg::with_name("all-features")
+//                 .long("all-features")
+//                 .takes_value(false)
+//                 .help("Activate all available features"),
+//         )
+//         // TODO, support additional parameters to KLEE
+//         .arg(
+//             Arg::with_name("klee")
+//                 .long("klee")
+//                 .short("k")
+//                 .help("Run KLEE test generation [default enabled unless --replay]"),
+//         )
+//         .arg(
+//             Arg::with_name("replay")
+//                 .long("replay")
+//                 .short("r")
+//                 .help("Generate replay binary in target directory"),
+//         )
+//         .arg(
+//             Arg::with_name("gdb")
+//                 .long("gdb")
+//                 .short("g")
+//                 .help("Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the `gdb` working directory, if unset `gdb` will execute in the current working directory"),
+//         )
+//         .get_matches();
+
+//     let is_example = matches.is_present("example");
+//     let is_binary = matches.is_present("bin");
+//     let verbose = matches.is_present("verbose");
+//     let is_release = matches.is_present("release");
+//     let is_replay = matches.is_present("replay");
+//     let is_ktest = matches.is_present("klee");
+//     let is_gdb = matches.is_present("gdb");
+
+//     // let target_flag = matches.value_of("target"); // not currently supported
+
+//     // we rely on `clap` for either `example` or `bin`
+//     let file = if is_example {
+//         matches.value_of("example").unwrap()
+//     } else {
+//         matches.value_of("bin").unwrap()
+//     };
+
+//     // turn `cargo klee --example foo` into `cargo rustc --example foo -- (..)`
+//     let mut cargo = Command::new("cargo");
+//     cargo
+//         // compile using rustc
+//         .arg("rustc")
+//         // verbose output for debugging purposes
+//         .arg("-v");
+
+//     // set features, always including `klee-analysis`
+//     if matches.is_present("all-features") {
+//         cargo.arg("--all-features");
+//     } else {
+//         if let Some(features) = matches.value_of("features") {
+//             let mut vec: Vec<&str> = features.split(" ").collect::<Vec<&str>>();
+//             vec.push("klee-analysis");
+//             cargo.args(&["--features", &vec.join(" ")]);
+//         } else {
+//             cargo.args(&["--features", "klee-analysis"]);
+//         }
+//     }
+
+//     // select (single) application to compile
+//     // derive basic settings from `cargo`
+//     if is_example {
+//         cargo.args(&["--example", file]);
+//     } else {
+//         cargo.args(&["--bin", file]);
+//     }
+
+//     // default is debug mode
+//     if is_release {
+//         cargo.arg("--release");
+//     }
+
+//     cargo
+//         // enable shell coloring of result
+//         .arg("--color=always")
+//         .arg("--")
+//         // ignore linking
+//         .args(&["-C", "linker=true"])
+//         // force LTO, to get a single oject file
+//         .args(&["-C", "lto"])
+//         // output the LLVM-IR (.ll file) for KLEE analysis
+//         .arg("--emit=llvm-ir")
+//         // force panic=abort in all crates, override .cargo settings
+//         .env("RUSTFLAGS", "-C panic=abort");
+//     // TODO, force `incremental=false`, `codegen-units=1`?
+
+//     if verbose {
+//         eprintln!("\n{:?}\n", cargo);
+//     }
+
+//     // execute the command and unwrap the result into status
+//     let status = cargo.status()?;
+
+//     if !status.success() {
+//         return Ok(status.code().unwrap_or(1));
+//     }
+
+//     let cwd = env::current_dir()?;
+
+//     let meta = rustc_version::version_meta()?;
+//     let host = meta.host;
+
+//     let project = Project::query(cwd)?;
+
+//     let profile = if is_release {
+//         Profile::Release
+//     } else {
+//         Profile::Dev
+//     };
+
+//     let mut path: PathBuf = if is_example {
+//         project.path(Artifact::Example(file), profile, None, &host)?
+//     } else {
+//         project.path(Artifact::Bin(file), profile, None, &host)?
+//     };
+
+//     // llvm-ir file
+//     let mut ll = None;
+//     // most recently modified
+//     let mut mrm = SystemTime::UNIX_EPOCH;
+//     let prefix = format!("{}-", file.replace('-', "_"));
+
+//     path = path.parent().expect("unreachable").to_path_buf();
+
+//     if is_binary {
+//         path = path.join("deps"); // the .ll file is placed in ../deps
+//     }
+
+//     // lookup the latest .ll file
+//     // TODO: stable support for `metadata` from Cargo.
+//     for e in fs::read_dir(path)? {
+//         let e = e?;
+//         let p = e.path();
+
+//         if p.extension().map(|e| e == "ll").unwrap_or(false) {
+//             if p.file_stem()
+//                 .expect("unreachable")
+//                 .to_str()
+//                 .expect("unreachable")
+//                 .starts_with(&prefix)
+//             {
+//                 let modified = e.metadata()?.modified()?;
+//                 if ll.is_none() {
+//                     ll = Some(p);
+//                     mrm = modified;
+//                 } else {
+//                     if modified > mrm {
+//                         ll = Some(p);
+//                         mrm = modified;
+//                     }
+//                 }
+//             }
+//         }
+//     }
+
+//     let mut obj = ll.clone().unwrap();
+//     let replay_name = obj.with_file_name(file).with_extension("replay");
+
+//     // replay compilation
+//     if is_replay {
+//         // compile to object code for replay using `llc`
+//         let mut llc = Command::new("llc");
+//         llc.arg("-filetype=obj")
+//             .arg("-relocation-model=pic")
+//             .arg(ll.clone().unwrap());
+
+//         if verbose {
+//             eprintln!("\n{:?}\n", llc);
+//         }
+
+//         // TODO: better error handling, e.g., if `llc` is not installed/in path
+//         let status = llc.status()?;
+//         if !status.success() {
+//             println!("llc failed: {:?}", status.code().unwrap_or(1));
+//         } else {
+//             // compile to executable for replay using `clang`
+//             let mut clang = Command::new("clang");
+
+//             obj = obj.with_extension("o");
+
+//             clang
+//                 .arg(obj)
+//                 .arg("--rtlib=compiler-rt")
+//                 .arg("-lkleeRuntest")
+//                 .args(&["-o", replay_name.to_str().unwrap()]);
+
+//             if verbose {
+//                 eprintln!("\n{:?}\n", clang);
+//             }
+
+//             // TODO: better error handling, e.g., if `clang` in not installed/in path
+//             let status = clang.status()?;
+//             if !status.success() {
+//                 println!("clang failed: {:?}", status.code().unwrap_or(1));
+//             }
+//         }
+//     }
+
+//     // klee analysis
+//     if is_ktest || !is_replay {
+//         let mut klee = Command::new("klee");
+//         klee
+//             // --disable-very to suppress know issue in klee https://github.com/klee/klee/issues/937
+//             .arg("--disable-verify")
+//             // --silent-klee-assume, to silence provably false assumptions
+//             .arg("--silent-klee-assume")
+//             // ll file to analyse
+//             .arg(ll.unwrap());
+
+//         // execute the command and unwrap the result into status
+//         let status = klee.status()?;
+//         if !status.success() {
+//             return Ok(status.code().unwrap_or(1));
+//         }
+//     }
+
+//     // replay execution in `gdb`
+//     if is_gdb {
+//         let mut gdb = Command::new("gdb");
+//         if let Ok(cwd) = env::var("GDB_CWD") {
+//             // set gdb current dir to `GDB_CWD`
+//             gdb.current_dir(cwd);
+//             // set replay name to be loaded by `gdb`
+//             gdb.arg(replay_name);
+//         } else {
+//             // set gdb current dir to the target directory
+//             gdb.current_dir(replay_name.parent().unwrap());
+//             // set replay name to be loaded by gdb
+//             gdb.arg(replay_name.file_name().unwrap());
+//         };
+
+//         if verbose {
+//             eprintln!("\n{:?}\n", gdb);
+//         }
+
+//         // TODO: better error handling, e.g., if `gdb` is not installed/in path
+//         let status = gdb.status()?;
+//         if !status.success() {
+//             println!("gdb failed: {:?}", status.code().unwrap_or(1));
+//         }
+//     }
+//     // return to shell without error
+//     Ok(0)
+// }