diff --git a/.gitignore b/.gitignore
index 6ad9b1bb..7b621d8f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@
 **/*.png
 **/*.s
 .DS_Store
+.z3-trace
diff --git a/Cargo.lock b/Cargo.lock
index d933aa03..3ae60423 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,9 +2,9 @@
 # It is not intended for manual editing.
 [[package]]
 name = "aho-corasick"
-version = "0.7.14"
+version = "0.7.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b476ce7103678b0c6d3d395dbbae31d48ff910bd28be979ba5d48c6351131d0d"
+checksum = "7404febffaa47dac81aa44dba71523c9d069b1bdc50a77db41195149e17f68e5"
 dependencies = [
  "memchr",
 ]
@@ -283,6 +283,7 @@ dependencies = [
  "rand",
  "riscv-decode",
  "serial_test",
+ "z3",
 ]
 
 [[package]]
@@ -352,9 +353,9 @@ checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6"
 
 [[package]]
 name = "ppv-lite86"
-version = "0.2.9"
+version = "0.2.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c36fa947111f5c62a733b652544dd0016a43ce89619538a8ef92724a6f501a20"
+checksum = "ac74c624d6b2d21f425f752262f42188365d7b8ff1aff74c82e45136510a4857"
 
 [[package]]
 name = "proc-macro-error"
@@ -632,3 +633,23 @@ name = "winapi-x86_64-pc-windows-gnu"
 version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+
+[[package]]
+name = "z3"
+version = "0.7.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "aa17be9852c6c2a8de2ea0875350dc5f8626f3eaa6b683148753b827f1b39ce5"
+dependencies = [
+ "lazy_static",
+ "log",
+ "z3-sys",
+]
+
+[[package]]
+name = "z3-sys"
+version = "0.6.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "afa18ba5fbd4933e41ffb440c3fd91f91fe9cdb7310cce3ddfb6648563811de0"
+dependencies = [
+ "cmake",
+]
diff --git a/Cargo.toml b/Cargo.toml
index c0971942..da72ce19 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -6,20 +6,21 @@ edition = "2018"
 description = "Monster is a symbolic execution engine for 64-bit RISC-V code"
 
 [dependencies]
-goblin = "0.2"
-byteorder = "1.3.4"
+goblin = "~0.2.3"
+byteorder = "~1.3.4"
 clap = "3.0.0-beta.2"
 riscv-decode = { git = "https://github.com/cksystemsgroup/riscv-decode" }
-petgraph = "0.5.1"
-rand = "0.7.3"
+petgraph = "~0.5.1"
+rand = "~0.7.3"
 boolector = { version = "0.4", git = "https://github.com/finga/boolector-rs", branch = "boolector-src", features = ["vendored"] }
-modinverse = "0.1.1"
-log = "0.4"
-env_logger = "0.8.1"
-bytesize = "1.0.1"
+z3 = { version = "~0.7.1", features = ["static-link-z3"] }
+modinverse = "~0.1.1"
+log = "~0.4.11"
+env_logger = "~0.8.1"
+bytesize = "~1.0.1"
 
 [dev-dependencies]
-serial_test = "0.4.0"
+serial_test = "~0.4.0"
 
 [dev-dependencies.cargo-husky]
 version = "1"
diff --git a/README.md b/README.md
index 90a67941..547147c0 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,9 @@
 # monster
 Monster is a symbolic execution engine for 64-bit RISC-V code
 
-# Toolchain setup
-## Install rust
+### Toolchain setup
+
+#### Linux and Unix-like OS
 1. Bootstrap rust
 ```
 $ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
@@ -21,25 +22,31 @@ $ echo 'export PATH="$HOME/.cargo/bin:$PATH"' >> ~/.zshrc && source ~/.zshrc
 $ cargo install cross
 $ cargo install mdbook
 $ cargo install mdbook-linkcheck
-$ cargo install --git https://github.com/christianmoesl/mdbook-graphviz
+$ cargo install mdbook-graphviz
 ```
+5. install Docker and LLVM with your favorite package manager
 
-## Docker and llvm
-### Debian based
-5. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/engine/install/debian/)
-6. Make sure you have a recent version of clang/llvm (>= v9) installed:
+##### MacOS
+6. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/docker-for-mac/install/)
 ```
-$ apt install llvm
+$ brew cask install docker
 ```
-
-### Mac
-5. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/docker-for-mac/install/)
-6. Make sure you have a recent version of clang/llvm (>= v9) installed:
+7. Make sure you have a recent version of clang/llvm (>= v9) installed:
 ```
 $ brew install llvm
 ```
 
-## Build and test
+##### Debian based
+6. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/engine/install/debian/)
+7. Make sure you have a recent version of clang/llvm (>= v9) installed:
+```
+$ apt install llvm
+```
+
+#### Windows
+We do not support Windows directly. But someone can use WSL2 to run/develop for Monster.
+
+### Build and Test from Source
 7. Test your toolchain setup by compiling monster:
 ```
 $ cargo build --locked
@@ -48,3 +55,4 @@ $ cargo build --locked
 ```
 $ cargo test --locked
 ```
+
diff --git a/src/boolector.rs b/src/boolector.rs
index 4c9027d1..920ef15f 100644
--- a/src/boolector.rs
+++ b/src/boolector.rs
@@ -1,127 +1,101 @@
 use crate::bitvec::BitVector;
 use crate::solver::{Assignment, Solver};
 use crate::symbolic_state::{
-    BVOperator, Formula,
+    get_operands, BVOperator, Formula,
     Node::{Constant, Input, Operator},
-    OperandSide,
+    SymbolId,
 };
 use boolector::{
     option::{BtorOption, ModelGen, OutputFileFormat},
     Btor, SolverResult, BV,
 };
-use log::debug;
-use petgraph::{graph::NodeIndex, Direction};
 use std::collections::HashMap;
 use std::rc::Rc;
 
-fn solve(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
-    let solver = Rc::new(Btor::new());
-    solver.set_opt(BtorOption::ModelGen(ModelGen::All));
-    solver.set_opt(BtorOption::Incremental(true));
-    solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2));
-
-    let mut bvs = HashMap::new();
-    let bv = traverse(graph, root, &solver, &mut bvs);
-    bv.assert();
+pub struct Boolector {}
 
-    if let SolverResult::Sat = solver.sat() {
-        let assignments = graph
-            .node_indices()
-            .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap()))
-            .collect();
+impl Boolector {
+    pub fn new() -> Self {
+        Self {}
+    }
+}
 
-        Some(assignments)
-    } else {
-        None
+impl Default for Boolector {
+    fn default() -> Self {
+        Self::new()
     }
 }
 
-fn get_operands(
-    graph: &Formula,
-    node: NodeIndex,
-    solver: &Rc<Btor>,
-    bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>,
-) -> (BV<Rc<Btor>>, Option<BV<Rc<Btor>>>) {
-    let mut operands = graph.neighbors_directed(node, Direction::Incoming).detach();
+impl Solver for Boolector {
+    fn name() -> &'static str {
+        "Boolector"
+    }
 
-    match operands.next(graph) {
-        Some(p) if graph[p.0] == OperandSide::Lhs => (traverse(graph, p.1, solver, bvs), {
-            if let Some(node) = operands.next(graph) {
-                Some(traverse(graph, node.1, solver, bvs))
-            } else {
-                None
-            }
-        }),
-        Some(p) if graph[p.0] == OperandSide::Rhs => (
-            traverse(graph, p.1, solver, bvs),
-            if let Some(node) = operands.next(graph) {
-                Some(traverse(graph, node.1, solver, bvs))
-            } else {
-                None
-            },
-        ),
-        _ => unreachable!(),
+    fn solve_impl(&mut self, graph: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+        let solver = Rc::new(Btor::new());
+        solver.set_opt(BtorOption::ModelGen(ModelGen::All));
+        solver.set_opt(BtorOption::Incremental(true));
+        solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2));
+
+        let mut bvs = HashMap::new();
+        let bv = traverse(graph, root, &solver, &mut bvs);
+        bv.assert();
+
+        if let SolverResult::Sat = solver.sat() {
+            let assignments = graph
+                .node_indices()
+                .filter(|i| matches!(graph[*i], Input(_)))
+                .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap()))
+                .collect();
+
+            Some(assignments)
+        } else {
+            None
+        }
     }
 }
 
 fn traverse<'a>(
     graph: &Formula,
-    node: NodeIndex,
+    node: SymbolId,
     solver: &'a Rc<Btor>,
-    bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>,
+    bvs: &mut HashMap<SymbolId, BV<Rc<Btor>>>,
 ) -> BV<Rc<Btor>> {
-    let bv = match &graph[node] {
-        Operator(op) => {
-            match get_operands(graph, node, solver, bvs) {
+    let bv =
+        match &graph[node] {
+            Operator(op) => match get_operands(graph, node) {
                 (lhs, Some(rhs)) => {
                     match op {
-                        BVOperator::Add => lhs.add(&rhs),
-                        BVOperator::Sub => lhs.sub(&rhs),
-                        BVOperator::Mul => lhs.mul(&rhs),
-                        BVOperator::Equals => lhs._eq(&rhs),
-                        BVOperator::BitwiseAnd => lhs.and(&rhs),
-                        //BVOperator::GreaterThan => lhs.ugt(&rhs),
+                        BVOperator::Add => traverse(graph, lhs, solver, bvs)
+                            .add(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Sub => traverse(graph, lhs, solver, bvs)
+                            .sub(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Mul => traverse(graph, lhs, solver, bvs)
+                            .mul(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Equals => traverse(graph, lhs, solver, bvs)
+                            ._eq(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::BitwiseAnd => traverse(graph, lhs, solver, bvs)
+                            .and(&traverse(graph, rhs, solver, bvs)),
                         i => unimplemented!("binary operator: {:?}", i),
                     }
                 }
                 (lhs, None) => match op {
-                    BVOperator::Not => lhs._eq(&BV::from_u64(solver.clone(), 0, 1)),
+                    BVOperator::Not => {
+                        traverse(graph, lhs, solver, bvs)._eq(&BV::from_u64(solver.clone(), 0, 1))
+                    }
                     i => unimplemented!("unary operator: {:?}", i),
                 },
+            },
+            Input(name) => {
+                if let Some(value) = bvs.get(&node) {
+                    value.clone()
+                } else {
+                    BV::new(solver.clone(), 64, Some(name))
+                }
             }
-        }
-        Input(name) => {
-            if let Some(value) = bvs.get(&node) {
-                value.clone()
-            } else {
-                BV::new(solver.clone(), 64, Some(name))
-            }
-        }
-        Constant(c) => BV::from_u64(solver.clone(), *c, 64),
-    };
+            Constant(c) => BV::from_u64(solver.clone(), *c, 64),
+        };
 
     bvs.insert(node, bv.clone());
     bv
 }
-
-pub struct Boolector {}
-
-impl Boolector {
-    pub fn new() -> Self {
-        Self {}
-    }
-}
-
-impl Default for Boolector {
-    fn default() -> Self {
-        Self::new()
-    }
-}
-
-impl Solver for Boolector {
-    fn solve(&mut self, graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
-        debug!("try to solve with Boolector");
-
-        time_debug!("finished solving formula", { solve(graph, root) })
-    }
-}
diff --git a/src/cli.rs b/src/cli.rs
index 494d7b79..ccc5ee75 100644
--- a/src/cli.rs
+++ b/src/cli.rs
@@ -1,6 +1,7 @@
 use clap::{crate_authors, crate_description, crate_name, crate_version, App, AppSettings, Arg};
 
 pub const LOGGING_LEVELS: [&str; 5] = ["trace", "debug", "info", "warn", "error"];
+pub const SOLVER: [&str; 3] = ["monster", "boolector", "z3"];
 
 pub fn args() -> App<'static> {
     App::new(crate_name!())
@@ -70,8 +71,8 @@ pub fn args() -> App<'static> {
                         .short('s')
                         .long("solver")
                         .takes_value(true)
-                        .possible_values(&["monster", "boolector"])
-                        .default_value("monster"),
+                        .possible_values(&SOLVER)
+                        .default_value(SOLVER[0]),
                 ),
         )
         .setting(AppSettings::SubcommandRequiredElseHelp)
diff --git a/src/engine.rs b/src/engine.rs
index 9a6e7a01..0804d17b 100644
--- a/src/engine.rs
+++ b/src/engine.rs
@@ -4,8 +4,9 @@ use crate::{
     cfg::build_cfg_from_file,
     elf::Program,
     exploration_strategy::{ExplorationStrategy, ShortestPathStrategy},
-    solver::{NativeSolver, Solver},
+    solver::{MonsterSolver, Solver},
     symbolic_state::{Query, SymbolId, SymbolicState},
+    z3::Z3,
 };
 use byteorder::{ByteOrder, LittleEndian};
 use bytesize::ByteSize;
@@ -25,6 +26,7 @@ pub enum SyscallId {
 pub enum Backend {
     Monster,
     Boolector,
+    Z3,
 }
 
 // TODO: What should the engine return as result?
@@ -35,7 +37,7 @@ pub fn execute(input: &Path, with: Backend) -> Result<(), String> {
 
     match with {
         Backend::Monster => {
-            let solver = Rc::new(RefCell::new(NativeSolver::new()));
+            let solver = Rc::new(RefCell::new(MonsterSolver::new()));
             let state = Box::new(SymbolicState::new(solver));
 
             let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
@@ -48,6 +50,14 @@ pub fn execute(input: &Path, with: Backend) -> Result<(), String> {
 
             let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
 
+            executor.run();
+        }
+        Backend::Z3 => {
+            let solver = Rc::new(RefCell::new(Z3::new()));
+            let state = Box::new(SymbolicState::new(solver));
+
+            let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+
             executor.run();
         }
     }
diff --git a/src/lib.rs b/src/lib.rs
index 803a995d..cea785fc 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -12,3 +12,4 @@ pub mod exploration_strategy;
 pub mod solver;
 pub mod symbolic_state;
 pub mod ternary;
+pub mod z3;
diff --git a/src/main.rs b/src/main.rs
index a4357e4a..fe9bfc3f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -61,11 +61,15 @@ fn main() {
                 let input = Path::new(args.value_of("input-file").unwrap());
                 let solver = args.value_of("solver").unwrap();
 
-                match solver {
-                    "monster" => engine::execute(input, engine::Backend::Monster),
-                    "boolector" => engine::execute(input, engine::Backend::Boolector),
-                    _ => unreachable!(),
-                }
+                engine::execute(
+                    input,
+                    match solver {
+                        "monster" => engine::Backend::Monster,
+                        "boolector" => engine::Backend::Boolector,
+                        "z3" => engine::Backend::Z3,
+                        _ => unreachable!(),
+                    },
+                )
             });
         }
         _ => unreachable!(),
diff --git a/src/solver.rs b/src/solver.rs
index fb5638cf..922a8fcd 100644
--- a/src/solver.rs
+++ b/src/solver.rs
@@ -1,7 +1,7 @@
 #![allow(clippy::many_single_char_names)]
 
 use crate::bitvec::*;
-use crate::symbolic_state::{BVOperator, Formula, Node, OperandSide, SymbolId as NodeIndex};
+use crate::symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId};
 use crate::ternary::*;
 use log::{debug, log_enabled, trace, Level};
 use petgraph::{visit::EdgeRef, Direction};
@@ -10,38 +10,46 @@ use rand::{random, Rng};
 pub type Assignment<T> = Vec<T>;
 
 pub trait Solver {
-    fn solve(&mut self, formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>>;
+    fn name() -> &'static str;
+
+    fn solve(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+        debug!("try to solve with {} solver", Self::name());
+
+        time_debug!("finished solving formula", {
+            self.solve_impl(formula, root)
+        })
+    }
+
+    fn solve_impl(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>>;
 }
 
-pub struct NativeSolver {}
+pub struct MonsterSolver {}
 
-impl Default for NativeSolver {
+impl Default for MonsterSolver {
     fn default() -> Self {
         Self::new()
     }
 }
 
-impl NativeSolver {
+impl MonsterSolver {
     pub fn new() -> Self {
         Self {}
     }
 }
 
-impl Solver for NativeSolver {
-    fn solve(&mut self, formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
-        debug!("try to solve with native solver");
-
-        time_debug!("finished solving formula", { solve(formula, root) })
+impl Solver for MonsterSolver {
+    fn name() -> &'static str {
+        "Monster"
     }
-}
 
-pub fn solve(formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
-    let ab = initialize_ab(formula);
-    let at = compute_at(formula);
+    fn solve_impl(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+        let ab = initialize_ab(formula);
+        let at = compute_at(formula);
 
-    let result = sat(formula, root, at, ab);
+        let result = sat(formula, root, at, ab);
 
-    Some(result)
+        Some(result)
+    }
 }
 
 // short-circuiting implies
@@ -107,7 +115,7 @@ fn is_consistent(op: BVOperator, x: TernaryBitVector, t: BitVector) -> bool {
     }
 }
 
-fn is_leaf(formula: &Formula, idx: NodeIndex) -> bool {
+fn is_leaf(formula: &Formula, idx: SymbolId) -> bool {
     let incoming = formula.edges_directed(idx, Direction::Incoming).count();
 
     incoming == 0
@@ -165,30 +173,32 @@ fn initialize_ab(formula: &Formula) -> Assignment<BitVector> {
 // otherwise selects an input undeterministically
 fn select(
     f: &Formula,
-    idx: NodeIndex,
+    idx: SymbolId,
     t: BitVector,
     at: &[TernaryBitVector],
     ab: &[BitVector],
-) -> (NodeIndex, NodeIndex, OperandSide) {
-    let (lhs, rhs) = parents(f, idx);
-
-    fn is_constant(f: &Formula, n: NodeIndex) -> bool {
-        matches!(f[n], Node::Constant(_))
-    }
+) -> (SymbolId, SymbolId, OperandSide) {
+    if let (lhs, Some(rhs)) = get_operands(f, idx) {
+        fn is_constant(f: &Formula, n: SymbolId) -> bool {
+            matches!(f[n], Node::Constant(_))
+        }
 
-    #[allow(clippy::if_same_then_else)]
-    if is_constant(f, lhs) {
-        (rhs, lhs, OperandSide::Rhs)
-    } else if is_constant(f, rhs) {
-        (lhs, rhs, OperandSide::Lhs)
-    } else if is_essential(f, lhs, OperandSide::Lhs, rhs, t, at, ab) {
-        (lhs, rhs, OperandSide::Lhs)
-    } else if is_essential(f, rhs, OperandSide::Rhs, lhs, t, at, ab) {
-        (rhs, lhs, OperandSide::Rhs)
-    } else if random() {
-        (rhs, lhs, OperandSide::Rhs)
+        #[allow(clippy::if_same_then_else)]
+        if is_constant(f, lhs) {
+            (rhs, lhs, OperandSide::Rhs)
+        } else if is_constant(f, rhs) {
+            (lhs, rhs, OperandSide::Lhs)
+        } else if is_essential(f, lhs, OperandSide::Lhs, rhs, t, at, ab) {
+            (lhs, rhs, OperandSide::Lhs)
+        } else if is_essential(f, rhs, OperandSide::Rhs, lhs, t, at, ab) {
+            (rhs, lhs, OperandSide::Rhs)
+        } else if random() {
+            (rhs, lhs, OperandSide::Rhs)
+        } else {
+            (lhs, rhs, OperandSide::Lhs)
+        }
     } else {
-        (lhs, rhs, OperandSide::Lhs)
+        panic!("can only select path for binary operators")
     }
 }
 
@@ -314,9 +324,9 @@ const CHOOSE_INVERSE: f64 = 0.90;
 #[allow(clippy::too_many_arguments)]
 fn value(
     f: &Formula,
-    n: NodeIndex,
-    nx: NodeIndex,
-    ns: NodeIndex,
+    n: SymbolId,
+    nx: SymbolId,
+    ns: SymbolId,
     side: OperandSide,
     t: BitVector,
     at: &[TernaryBitVector],
@@ -349,9 +359,9 @@ fn value(
 
 fn is_essential(
     formula: &Formula,
-    this: NodeIndex,
+    this: SymbolId,
     on_side: OperandSide,
-    other: NodeIndex,
+    other: SymbolId,
     t: BitVector,
     at: &[TernaryBitVector],
     ab: &[BitVector],
@@ -366,28 +376,14 @@ fn is_essential(
     }
 }
 
-fn parent(f: &Formula, n: NodeIndex) -> NodeIndex {
+fn get_operand(f: &Formula, n: SymbolId) -> SymbolId {
     f.edges_directed(n, Direction::Incoming)
         .next()
         .unwrap()
         .source()
 }
 
-fn parents(f: &Formula, n: NodeIndex) -> (NodeIndex, NodeIndex) {
-    fn target_by_side(f: &Formula, n: NodeIndex, side: OperandSide) -> NodeIndex {
-        f.edges_directed(n, Direction::Incoming)
-            .find(|e| *e.weight() == side)
-            .unwrap()
-            .source()
-    }
-
-    let lhs = target_by_side(f, n, OperandSide::Lhs);
-    let rhs = target_by_side(f, n, OperandSide::Rhs);
-
-    (lhs, rhs)
-}
-
-fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, v: BitVector) {
+fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, v: BitVector) {
     ab[n.index()] = v;
 
     trace!("update: x{} <- {:#x}", n.index(), v.0);
@@ -396,49 +392,53 @@ fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex,
         .for_each(|n| propagate_assignment(f, ab, n));
 }
 
-fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex) {
-    fn update_binary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, s: &str, op: Op)
+fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId) {
+    fn update_binary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
     where
         Op: FnOnce(BitVector, BitVector) -> BitVector,
     {
-        let (lhs, rhs) = parents(f, n);
-
-        let result = op(ab[lhs.index()], ab[rhs.index()]);
-
-        trace!(
-            "propagate: x{} := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}",
-            n.index(),
-            lhs.index(),
-            ab[lhs.index()].0,
-            s,
-            rhs.index(),
-            ab[rhs.index()].0,
-            n.index(),
-            result.0
-        );
+        if let (lhs, Some(rhs)) = get_operands(f, n) {
+            let result = op(ab[lhs.index()], ab[rhs.index()]);
+
+            trace!(
+                "propagate: x{} := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}",
+                n.index(),
+                lhs.index(),
+                ab[lhs.index()].0,
+                s,
+                rhs.index(),
+                ab[rhs.index()].0,
+                n.index(),
+                result.0
+            );
 
-        ab[n.index()] = result;
+            ab[n.index()] = result;
+        } else {
+            panic!("can not update binary operator with 1 operand")
+        }
     }
 
-    fn update_unary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, s: &str, op: Op)
+    fn update_unary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
     where
         Op: FnOnce(BitVector) -> BitVector,
     {
-        let p = parent(f, n);
-
-        let result = op(ab[p.index()]);
+        if let (p, None) = get_operands(f, n) {
+            let result = op(ab[p.index()]);
 
-        trace!(
-            "propagate: x{} := {}x{}({:#x}) |- x{} <- {:#x}",
-            n.index(),
-            s,
-            p.index(),
-            ab[p.index()].0,
-            n.index(),
-            result.0
-        );
+            trace!(
+                "propagate: x{} := {}x{}({:#x}) |- x{} <- {:#x}",
+                n.index(),
+                s,
+                p.index(),
+                ab[p.index()].0,
+                n.index(),
+                result.0
+            );
 
-        ab[n.index()] = result;
+            ab[n.index()] = result;
+        } else {
+            panic!("can not update unary operator with more than one operand")
+        }
     }
 
     match &f[n] {
@@ -474,7 +474,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeInde
 // can only handle one Equals constrain with constant
 fn sat(
     formula: &Formula,
-    root: NodeIndex,
+    root: SymbolId,
     at: Assignment<TernaryBitVector>,
     mut ab: Assignment<BitVector>,
 ) -> Assignment<BitVector> {
@@ -491,7 +491,7 @@ fn sat(
             let (v, nx) = match formula[n] {
                 Node::Operator(op) => {
                     if op.is_unary() {
-                        let nx = parent(formula, n);
+                        let nx = get_operand(formula, n);
 
                         let x = at[nx.index()];
 
@@ -575,7 +575,7 @@ fn sat(
 mod tests {
     use super::*;
 
-    fn create_formula_with_input() -> (Formula, NodeIndex) {
+    fn create_formula_with_input() -> (Formula, SymbolId) {
         let mut formula = Formula::new();
 
         let input = Node::Input(String::from("x0"));
@@ -586,10 +586,10 @@ mod tests {
 
     fn add_equals_constrain(
         formula: &mut Formula,
-        to: NodeIndex,
+        to: SymbolId,
         on: OperandSide,
         constant: u64,
-    ) -> NodeIndex {
+    ) -> SymbolId {
         let constrain = Node::Operator(BVOperator::Equals);
         let constrain_idx = formula.add_node(constrain);
 
@@ -608,7 +608,8 @@ mod tests {
 
         let root = add_equals_constrain(&mut formula, input_idx, OperandSide::Lhs, 10);
 
-        let result = solve(&formula, root);
+        let mut solver = MonsterSolver::default();
+        let result = solver.solve(&formula, root);
 
         assert!(result.is_some(), "has result for trivial equals constrain");
         assert_eq!(
@@ -633,7 +634,8 @@ mod tests {
 
         let root = add_equals_constrain(&mut formula, instr_idx, OperandSide::Lhs, 10);
 
-        let result = solve(&formula, root);
+        let mut solver = MonsterSolver::default();
+        let result = solver.solve(&formula, root);
 
         assert!(result.is_some(), "has result for trivial add op");
         assert_eq!(
diff --git a/src/symbolic_state.rs b/src/symbolic_state.rs
index 401c1d1b..a60f019c 100644
--- a/src/symbolic_state.rs
+++ b/src/symbolic_state.rs
@@ -73,6 +73,7 @@ pub enum Node {
     Operator(BVOperator),
 }
 
+pub type Formula = Graph<Node, OperandSide>;
 pub type SymbolId = NodeIndex;
 
 fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator {
@@ -85,7 +86,23 @@ fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator {
     }
 }
 
-pub type Formula = Graph<Node, OperandSide>;
+pub fn get_operands(graph: &Formula, sym: SymbolId) -> (SymbolId, Option<SymbolId>) {
+    let mut iter = graph.neighbors_directed(sym, Direction::Incoming).detach();
+
+    let lhs = iter
+        .next(graph)
+        .expect("get_operands() should not be called on operators without operands")
+        .1;
+
+    let rhs = iter.next(graph).map(|n| n.1);
+
+    assert!(
+        iter.next(graph) == None,
+        "operators with arity 1 or 2 are supported only"
+    );
+
+    (lhs, rhs)
+}
 
 #[derive(Debug)]
 pub struct SymbolicState<S>
diff --git a/src/z3.rs b/src/z3.rs
new file mode 100644
index 00000000..93942336
--- /dev/null
+++ b/src/z3.rs
@@ -0,0 +1,118 @@
+use crate::bitvec::BitVector;
+use crate::solver::{Assignment, Solver};
+use crate::symbolic_state::{
+    get_operands, BVOperator, Formula,
+    Node::{Constant, Input, Operator},
+    SymbolId,
+};
+use std::collections::HashMap;
+use z3::{
+    ast::{Ast, Dynamic, BV},
+    Config, Context, SatResult, Solver as Z3Solver,
+};
+
+pub struct Z3 {}
+
+impl Z3 {
+    pub fn new() -> Self {
+        Self {}
+    }
+}
+
+impl Default for Z3 {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+impl Solver for Z3 {
+    fn name() -> &'static str {
+        "Z3"
+    }
+
+    fn solve_impl(&mut self, graph: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+        let config = Config::default();
+        let ctx = Context::new(&config);
+
+        let mut bvs = HashMap::new();
+        let bv = traverse(graph, root, &ctx, &mut bvs);
+
+        let solver = Z3Solver::new(&ctx);
+
+        solver.assert(&bv.as_bool().unwrap());
+
+        match solver.check() {
+            SatResult::Sat => {
+                let m = solver.get_model().unwrap();
+
+                Some(
+                    graph
+                        .node_indices()
+                        .filter(|i| matches!(graph[*i], Input(_)))
+                        .map(|i| {
+                            let input_bv = bvs.get(&i).unwrap().as_bv().unwrap();
+                            let result_bv = m.eval(&input_bv).unwrap();
+                            let result_value = result_bv.as_u64().unwrap();
+
+                            BitVector(result_value)
+                        })
+                        .collect(),
+                )
+            }
+            _ => None,
+        }
+    }
+}
+
+macro_rules! traverse_binary {
+    ($lhs:expr, $op:ident, $rhs:expr, $graph:expr, $ctx:expr, $bvs:expr) => {
+        Dynamic::from(
+            traverse($graph, $lhs, $ctx, $bvs)
+                .as_bv()
+                .expect("An AST node of type BitVector should be at this position")
+                .$op(
+                    &traverse($graph, $rhs, $ctx, $bvs)
+                        .as_bv()
+                        .expect("An AST node of type BitVector should be at this position"),
+                ),
+        )
+    };
+}
+
+fn traverse<'ctx>(
+    graph: &Formula,
+    node: SymbolId,
+    ctx: &'ctx Context,
+    bvs: &mut HashMap<SymbolId, Dynamic<'ctx>>,
+) -> Dynamic<'ctx> {
+    let bv = match &graph[node] {
+        Operator(op) => match get_operands(graph, node) {
+            (lhs, Some(rhs)) => match op {
+                BVOperator::Add => traverse_binary!(lhs, bvadd, rhs, graph, ctx, bvs),
+                BVOperator::Sub => traverse_binary!(lhs, bvsub, rhs, graph, ctx, bvs),
+                BVOperator::Mul => traverse_binary!(lhs, bvmul, rhs, graph, ctx, bvs),
+                BVOperator::Equals => traverse_binary!(lhs, _eq, rhs, graph, ctx, bvs),
+                BVOperator::BitwiseAnd => traverse_binary!(lhs, bvand, rhs, graph, ctx, bvs),
+                i => unimplemented!("binary operator: {:?}", i),
+            },
+            (lhs, None) => match op {
+                BVOperator::Not => {
+                    let zero = BV::from_u64(ctx, 0, 64);
+                    Dynamic::from(traverse(graph, lhs, ctx, bvs)._eq(&Dynamic::from(zero)))
+                }
+                i => unimplemented!("unary operator: {:?}", i),
+            },
+        },
+        Input(name) => {
+            if let Some(value) = bvs.get(&node) {
+                value.clone()
+            } else {
+                Dynamic::from(BV::new_const(ctx, name.clone(), 64))
+            }
+        }
+        Constant(cst) => Dynamic::from(BV::from_u64(ctx, *cst, 64)),
+    };
+
+    bvs.insert(node, bv.clone());
+    bv
+}
diff --git a/tests/engine.rs b/tests/engine.rs
index 09676117..4dad5a89 100644
--- a/tests/engine.rs
+++ b/tests/engine.rs
@@ -29,3 +29,9 @@ fn execute_riscu_with_boolector_solver() {
     execute_riscu_with_monster("symbolic/arithmetic.c", engine::Backend::Boolector);
     execute_riscu_with_monster("symbolic/if-else.c", engine::Backend::Boolector);
 }
+
+#[test]
+fn execute_riscu_with_z3_solver() {
+    execute_riscu_with_monster("symbolic/arithmetic.c", engine::Backend::Z3);
+    execute_riscu_with_monster("symbolic/if-else.c", engine::Backend::Z3);
+}