diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 0cf5ed3..f7e2932 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -183,6 +183,25 @@ jobs:
         run: |
           cargo run --release -p patronus-egraphs-cond-synth -- --check-cond mult-to-add
 
+  smt-simplify:
+    name: Test SMT Simplifier
+    runs-on: ubuntu-24.04
+    timeout-minutes: 5
+    strategy:
+      matrix:
+        toolchain:
+          - stable
+
+    steps:
+      - name: Update Rust to ${{ matrix.toolchain }}
+        run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
+      - uses: actions/checkout@v4
+      - name: Build
+        run: cargo build --verbose --release -p simplify
+      - name: run
+        run: cargo run --release -p simplify -- in.smt out.smt
+
+
   semver:
     name: Check Semantic Versioning of Patronus
     runs-on: ubuntu-24.04
diff --git a/Cargo.toml b/Cargo.toml
index 6c6c38d..0452efe 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,6 +1,6 @@
 [workspace]
 resolver = "2"
-members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim"]
+members = ["patronus", "patronus-egraphs", "patronus-dse", "tools/bmc", "tools/egraphs-cond-synth", "tools/sim", "tools/simplify"]
 
 [workspace.package]
 edition = "2021"
diff --git a/tools/simplify/Cargo.toml b/tools/simplify/Cargo.toml
new file mode 100644
index 0000000..fba0d75
--- /dev/null
+++ b/tools/simplify/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "simplify"
+version = "0.1.0"
+edition.workspace = true
+authors.workspace = true
+repository.workspace = true
+readme.workspace = true
+license.workspace = true
+rust-version.workspace = true
+
+[dependencies]
+patronus.workspace = true
+clap.workspace = true
diff --git a/tools/simplify/src/main.rs b/tools/simplify/src/main.rs
new file mode 100644
index 0000000..2c9dcbb
--- /dev/null
+++ b/tools/simplify/src/main.rs
@@ -0,0 +1,24 @@
+// Copyright 2024 Cornell University
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <laeufer@cornell.edu>
+
+use clap::Parser;
+use patronus::expr::*;
+use patronus::*;
+
+#[derive(Parser, Debug)]
+#[command(name = "simplify")]
+#[command(author = "Kevin Laeufer <laeufer@berkeley.edu>")]
+#[command(version)]
+#[command(about = "Parses a SMT file, simplifies it and writes the simplified version to an output file.", long_about = None)]
+struct Args {
+    #[arg(value_name = "INPUT", index = 1)]
+    input_file: String,
+    #[arg(value_name = "OUTPUT", index = 2)]
+    output_file: String,
+}
+
+fn main() {
+    let args = Args::parse();
+    todo!();
+}
\ No newline at end of file