diff --git a/src/candidate_path.rs b/src/candidate_path.rs
index 105e244a..4d8c0dc4 100644
--- a/src/candidate_path.rs
+++ b/src/candidate_path.rs
@@ -1,153 +1,114 @@
 use crate::cfg::ControlFlowGraph;
-use petgraph::graph::NodeIndex;
-use petgraph::visit::EdgeRef;
+use petgraph::{
+    algo::{all_simple_paths, has_path_connecting},
+    graph::NodeIndex,
+    Direction,
+};
 use riscv_decode::Instruction;
 
-pub struct CandidatePath<'a> {
-    pub root: NodeIndex, // instruction we want to evaluate (exit syscall, division with a potential 0 as divisor, ... )
-    pub path: ControlFlowGraph, // actual candidate path from the root to instuctions with no incoming edges and read syscalls
-    pub alternative_roots: Vec<NodeIndex>, // alternative roots for generating new candidate paths from the same control-flow graph (relevant for CandidatePath::next())
-    pub cfg: &'a ControlFlowGraph, // control-flow graph which this candidate path is extracted from
+pub type CandidatePath = (Vec<Instruction>, Vec<bool>);
+
+fn is_exit_node(g: &ControlFlowGraph, idx: NodeIndex) -> bool {
+    g.neighbors_directed(idx, Direction::Outgoing).count() == 0
+        && has_path_connecting(g, NodeIndex::new(0), idx, None)
 }
 
-#[allow(dead_code)]
-impl<'a> CandidatePath<'a> {
-    // may return a reference to a candidate path with a new path and root field
-    pub fn next(&'a mut self) -> Option<&mut CandidatePath> {
-        if let Some(root) = self.alternative_roots.pop() {
-            self.root = root;
-            self.path = ControlFlowGraph::new();
-            self.compute_candidate_path(self.root);
-            Some(self)
-        } else {
-            None
-        }
-    }
+// TODO: Remove all these temporary data structures (collect..)
+pub fn create_candidate_paths(cfg: &ControlFlowGraph) -> Vec<CandidatePath> {
+    cfg.node_indices()
+        .filter(|i| is_exit_node(cfg, *i))
+        .flat_map(|exit| {
+            all_simple_paths::<Vec<NodeIndex>, &ControlFlowGraph>(
+                cfg,
+                NodeIndex::new(0),
+                exit,
+                0,
+                None,
+            )
+        })
+        .map(|path| {
+            let instructions = path
+                .clone()
+                .into_iter()
+                .map(|idx| cfg[idx])
+                .collect::<Vec<Instruction>>();
 
-    // computes the candidate path using its cfg and a provided node, it populates its path field;
-    // to begin with, this function always gets invoked with a root node as parameter,
-    // it adds all "incoming neighbor nodes" (neighbors which are connected with an incoming edge) together with respective incoming edges to the path,
-    // then recusively calls itself with those neighboring nodes as parameter,
-    // thus propagating through the cfg, continuing to add neighboring nodes and edges
-    // the end nodes of the path are read syscalls or nodes with no incoming neighbors
-    fn compute_candidate_path(&mut self, node: NodeIndex) {
-        self.cfg
-            .neighbors_directed(node, petgraph::Incoming)
-            .for_each(|x| {
-                self.path.node_indices().for_each(|idx| {
-                    if self.cfg[x] == self.path[idx] {
-                        // node is already in path
-                    } else {
-                        self.path.add_node(self.cfg[x]);
-                    }
-                });
-                self.path.add_edge(x, node, None);
-                match self.cfg[x] {
-                    Instruction::Ecall => {
-                        if is_read(self.cfg, x) {
-                            // stop candidate path generation at read syscalls
-                        } else {
-                            self.compute_candidate_path(x);
+            let decisions = path
+                .clone()
+                .into_iter()
+                .enumerate()
+                .filter_map(|(i, idx)| {
+                    match cfg[idx] {
+                        Instruction::Beq(_) => {
+                            // a branch to the next idx is a decision for the false branch
+                            Some(idx.index() + 1 != path[i + 1].index())
                         }
+                        _ => None,
                     }
-                    _ => {
-                        self.compute_candidate_path(x);
-                    }
-                }
-            })
-    }
+                })
+                .collect::<Vec<bool>>();
 
-    // invokes find_roots() which populates the alternative_roots field of the new candidate path
-    // invokes compute_candidate_path() to populate its path field
-    pub fn generate_candidate_path(graph: &ControlFlowGraph) -> Option<CandidatePath> {
-        // find root nodes (exit syscall, division with a potential 0 as divisor) using a provided control-flow graph
-        fn find_roots(graph: &ControlFlowGraph) -> Option<Vec<NodeIndex>> {
-            let mut roots = vec![];
+            (instructions, decisions)
+        })
+        .collect()
+}
 
-            graph.node_indices().for_each(|idx| {
-                if let Instruction::Ecall = graph[idx] {
-                    if let Some(idx) = is_exit_point(graph, idx) {
-                        roots.push(idx);
-                    }
-                } else if let Instruction::Divu(_rtype) = graph[idx] {
-                    if let Some(idx) = is_exit_point(graph, idx) {
-                        roots.push(idx);
-                    }
-                };
-            });
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::cfg::*;
+    use serial_test::serial;
+    use std::env::current_dir;
+    use std::path::Path;
+    use std::process::Command;
+    use std::string::String;
 
-            if roots.is_empty() {
-                None
-            } else {
-                Some(roots)
-            }
-        }
+    // TODO: write a unit test without dependency on selfie and external files
+    #[test]
+    #[serial]
+    fn can_build_control_flow_graph() {
+        let cd = String::from(current_dir().unwrap().to_str().unwrap());
 
-        if let Some(mut alternative_roots) = find_roots(&graph) {
-            if let Some(root) = alternative_roots.pop() {
-                let mut candidate_path = CandidatePath {
-                    cfg: graph,
-                    path: ControlFlowGraph::new(),
-                    root,
-                    alternative_roots,
-                };
-                candidate_path.compute_candidate_path(candidate_path.root);
-                Some(candidate_path)
-            } else {
-                None
-            }
-        } else {
-            None
-        }
-    }
-}
+        // generate RISC-U binary with Selfie
+        let _ = Command::new("docker")
+            .arg("run")
+            .arg("-v")
+            .arg(cd + ":/opt/monster")
+            .arg("cksystemsteaching/selfie")
+            .arg("/opt/selfie/selfie")
+            .arg("-c")
+            .arg("/opt/monster/symbolic/division-by-zero-3-35.c")
+            .arg("-o")
+            .arg("/opt/monster/symbolic/division-by-zero-3-35.riscu.o")
+            .output();
 
-// checks if an instruction is a read syscall
-#[allow(dead_code)]
-fn is_read(graph: &ControlFlowGraph, idx: NodeIndex) -> bool {
-    match graph[NodeIndex::new(idx.index() - 1)] {
-        Instruction::Addi(a) => a.imm() == 63,
-        _ => false,
-    }
-}
+        let test_file = Path::new("symbolic/division-by-zero-3-35.riscu.o");
 
-// checks if an instruction is either a divu or an exit syscall
-#[allow(dead_code)]
-fn is_exit_point(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<NodeIndex> {
-    match graph[idx] {
-        // get division exit points
-        Instruction::Divu(_rtype) => Some(idx),
-        _ => match graph[NodeIndex::new(idx.index() - 1)] {
-            // get exit syscall exit points
-            Instruction::Addi(a) => {
-                if a.imm() == 93 {
-                    Some(idx)
-                } else {
-                    None
-                }
-            }
-            _ => None,
-        },
-    }
-}
+        let (graph, _, _) = build_from_file(test_file).unwrap();
 
-// extracts a trivial condidate path starting from the very last jump to an ecall (exit)
-#[allow(dead_code)]
-pub fn extract_trivial_candidate_path(graph: &ControlFlowGraph) -> Vec<Instruction> {
-    fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<NodeIndex> {
-        let edges = graph.edges_directed(idx, petgraph::Incoming);
-        if let Some(edge) = edges.last() {
-            Some(edge.source())
-        } else {
-            None
-        }
-    }
-    let mut path = vec![];
-    let mut idx = graph.node_indices().last().unwrap();
-    path.push(idx);
-    while let Some(n) = next(graph, idx) {
-        path.push(n);
-        idx = n;
+        let paths = create_candidate_paths(&graph).into_iter().count();
+
+        create_candidate_paths(&graph)
+            .into_iter()
+            .for_each(|(p, d)| {
+                let number_of_beqs = p
+                    .into_iter()
+                    .filter(|i| {
+                        if let Instruction::Beq(_) = i {
+                            true
+                        } else {
+                            false
+                        }
+                    })
+                    .count();
+                let number_of_decisions = d.len();
+
+                assert_eq!(number_of_beqs, number_of_decisions);
+            });
+
+        assert_eq!(
+            paths, 28,
+            "there are 28 possible candidate paths in division-by-zero-3-35"
+        );
     }
-    path.iter().map(|idx| graph[*idx]).collect()
 }
diff --git a/src/formula_graph.rs b/src/formula_graph.rs
index 1960db5a..402fca07 100644
--- a/src/formula_graph.rs
+++ b/src/formula_graph.rs
@@ -1,10 +1,8 @@
-use crate::cfg::ControlFlowGraph;
 use crate::elf::ElfMetadata;
 use crate::iterator::ForEachUntilSome;
 use byteorder::{ByteOrder, LittleEndian};
 use core::fmt;
 pub use petgraph::graph::NodeIndex;
-use petgraph::visit::EdgeRef;
 use petgraph::Graph;
 use riscv_decode::types::{BType, IType, RType, SType, UType};
 use riscv_decode::Instruction;
@@ -630,52 +628,11 @@ pub fn build_dataflow_graph(
     .generate_graph()
 }
 
-// Returns a path of RISC-U instructions and branch decisions (if true or false branch has been taken)
-// for a path with 1 BEQ instruction, the vector of branch decisions has the length of 1
-pub fn extract_candidate_path(graph: &ControlFlowGraph) -> (Vec<Instruction>, Vec<bool>) {
-    fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<(NodeIndex, Option<bool>)> {
-        let edges = graph.edges(idx);
-
-        if let Some(edge) = edges.last() {
-            let target = edge.target();
-
-            match graph[idx] {
-                Instruction::Beq(_) => {
-                    let next_idx = edge.target().index();
-
-                    if next_idx == idx.index() + 1 {
-                        Some((target, Some(false)))
-                    } else {
-                        Some((target, Some(true)))
-                    }
-                }
-                _ => Some((target, None)),
-            }
-        } else {
-            None
-        }
-    }
-    let mut path = vec![];
-    let mut branch_decisions = vec![];
-    let mut idx = graph.node_indices().next().unwrap();
-    path.push(idx);
-    while let Some(n) = next(graph, idx) {
-        path.push(n.0);
-        idx = n.0;
-
-        if let Some(branch_decision) = n.1 {
-            branch_decisions.push(branch_decision);
-        }
-    }
-    let instruction_path = path.iter().map(|idx| graph[*idx]).collect();
-
-    (instruction_path, branch_decisions)
-}
-
 // TODO: need to load data segment  => then write test
 #[cfg(test)]
 mod tests {
     use super::*;
+    use crate::candidate_path::create_candidate_paths;
     use crate::cfg;
     use petgraph::dot::Dot;
     use serial_test::serial;
@@ -710,7 +667,7 @@ mod tests {
 
         println!("{:?}", data_segment);
 
-        let (path, branch_decisions) = extract_candidate_path(&graph);
+        let (path, branch_decisions) = create_candidate_paths(&graph)[0].clone();
 
         println!("{:?}", path);
 
diff --git a/src/main.rs b/src/main.rs
index ef60ccf1..0a535be8 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -74,7 +74,8 @@ fn main() {
         }
         Some(("smt", _cfg_args)) => {
             handle_error(|| -> Result<(), String> {
-                use crate::formula_graph::{build_dataflow_graph, extract_candidate_path};
+                use crate::candidate_path::create_candidate_paths;
+                use crate::formula_graph::build_dataflow_graph;
                 use petgraph::dot::Dot;
                 use std::env::current_dir;
                 use std::fs::File;
@@ -102,7 +103,7 @@ fn main() {
 
                 // println!("{:?}", data_segment);
 
-                let (path, branch_decisions) = extract_candidate_path(&graph);
+                let (path, branch_decisions) = create_candidate_paths(&graph)[0].clone();
 
                 // println!("{:?}", path);