diff --git a/src/cli.rs b/src/cli.rs
index 0438d44b..14a1eee2 100644
--- a/src/cli.rs
+++ b/src/cli.rs
@@ -258,6 +258,25 @@ pub fn args() -> Command {
                         .allow_hyphen_values(true)
                         .num_args(1..)
                 )
+                .arg(
+                    Arg::new("stride")
+                        .help("Find unroll level where SMT solver times out")
+                        .short('l')
+                        .long("stride")
+                        .num_args(0)
+                        // TODO: Set base via argument
+                        // .value_name("NUMBER")
+                        // .value_parser(value_parser!(u64)),
+                )
+                .arg(
+                    Arg::new("time-budget")
+                        .help("Set an overall time budget in milliseconds")
+                        .short('g')
+                        .long("time-budget")
+                        .num_args(1)
+                        .value_name("NUMBER")
+                        .value_parser(value_parser!(u64))
+                )
         )
         .subcommand(
             Command::new("qubot")
diff --git a/src/main.rs b/src/main.rs
index 05c16f05..640a41ed 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -12,18 +12,29 @@ use crate::unicorn::codegen::compile_model_into_program;
 use crate::unicorn::dimacs_parser::load_dimacs_as_gatemodel;
 use crate::unicorn::emulate_loader::load_model_into_emulator;
 use crate::unicorn::memory::replace_memory;
-use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver};
+// use crate::unicorn::optimize::{
+//     optimize_model_with_input,
+//     optimize_model_with_solver
+// };
 use crate::unicorn::qubot::{InputEvaluator, Qubot};
 use crate::unicorn::sat_solver::solve_bad_states;
-use crate::unicorn::smt_solver::*;
-use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model};
+// use crate::unicorn::smt_solver::*;
+use crate::unicorn::unroller::renumber_model;
 use crate::unicorn::write_model;
+use crate::unicorn::horizon::compute_reasoning_horizon;
 
 use ::unicorn::disassemble::disassemble;
 use ::unicorn::emulate::EmulatorState;
 use anyhow::{Context, Result};
 use bytesize::ByteSize;
-use cli::{collect_arg_values, expect_arg, expect_optional_arg, LogLevel, SatType, SmtType};
+use cli::{
+    collect_arg_values,
+    expect_arg,
+    expect_optional_arg,
+    LogLevel,
+    SatType,
+    SmtType
+};
 use env_logger::{Env, TimestampPrecision};
 use riscu::load_object_file;
 use std::{
@@ -32,7 +43,7 @@ use std::{
     io::{stdout, Write},
     path::PathBuf,
     str::FromStr,
-    time::Duration,
+    time::Duration
 };
 
 fn main() -> Result<()> {
@@ -87,6 +98,8 @@ fn main() -> Result<()> {
             let input_is_dimacs = !is_beator && args.get_flag("from-dimacs");
             let compile_model = is_beator && args.get_flag("compile");
             let emulate_model = is_beator && args.get_flag("emulate");
+            let stride = args.get_flag("stride");
+            let solver_time_budget = args.get_one::<u64>("time-budget");
             let arg0 = expect_arg::<String>(args, "input-file")?;
             let extras = collect_arg_values(args, "extras");
 
@@ -114,32 +127,29 @@ fn main() -> Result<()> {
                     } else {
                         vec![]
                     };
-                    for n in 0..unroll_depth {
-                        unroll_model(&mut model, n);
-                        if has_concrete_inputs {
-                            optimize_model_with_input(&mut model, &mut input_values)
-                        }
-                    }
-                    if prune {
-                        prune_model(&mut model);
-                    }
+
                     let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms));
-                    match smt_solver {
-                        #[rustfmt::skip]
-                        SmtType::Generic => {
-                            optimize_model_with_solver::<none_impl::NoneSolver>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                        #[rustfmt::skip]
-                        #[cfg(feature = "boolector")]
-                        SmtType::Boolector => {
-                            optimize_model_with_solver::<boolector_impl::BoolectorSolver>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                        #[rustfmt::skip]
-                        #[cfg(feature = "z3")]
-                        SmtType::Z3 => {
-                            optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(&mut model, timeout, minimize, terminate_on_bad, one_query)
-                        },
-                    }
+                    
+                    let mut time_budget = solver_time_budget.map(
+                        |&ms| Duration::from_millis(ms)
+                    );
+
+                    // TODO: Refactor the subsequent loop (reasoning horizon)
+                    compute_reasoning_horizon(
+                        &mut model,
+                        has_concrete_inputs,
+                        &mut input_values,
+                        unroll_depth,
+                        prune,
+                        stride,
+                        &smt_solver,
+                        timeout,
+                        minimize,
+                        terminate_on_bad,
+                        one_query,
+                        &mut time_budget
+                    );
+
                     if renumber {
                         renumber_model(&mut model);
                     }
diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs
new file mode 100644
index 00000000..cb6297d1
--- /dev/null
+++ b/src/unicorn/horizon.rs
@@ -0,0 +1,257 @@
+use crate::unicorn::{Node, NodeRef, Model};
+use crate::cli::{SmtType};
+use crate::unicorn::unroller::{prune_model, unroll_model};
+use crate::unicorn::optimize::{
+    optimize_model_with_input,
+    optimize_model_with_solver,
+    // optimize_model_with_solver_n
+};
+use crate::unicorn::smt_solver::*;
+
+use log::{debug, warn};
+use std::{
+    cmp::min,
+    time::{Duration,Instant}
+};
+
+//
+// Public Interface
+//
+
+pub fn compute_reasoning_horizon(
+    model: &mut Model,
+    has_concrete_inputs: bool,
+    input_values: &mut Vec<u64>,
+    unroll_depth: usize,
+    prune: bool,
+    stride: bool,
+    smt_solver: &SmtType,
+    timeout: Option<Duration>,
+    minimize: bool,
+    terminate_on_bad: bool,
+    one_query: bool,
+    time_budget: &mut Option<Duration>
+) {
+    let has_time_budget = !time_budget.is_none();
+
+    let mut n: usize = if stride { 1 } else { unroll_depth };
+    let mut prev_n: usize = 0;
+
+    let mut exec_time = Duration::from_millis(0);
+
+    loop {
+        // TODO(1): Maybe we can get rid of this clone for each
+        // iteration, which is basically required if pruning is
+        // enabled. However, it is much faster this way than
+        // without pruning and not cloning the model.
+        let (elapsed, bad_states_initial) = reason(
+            &mut model.clone(),
+            has_concrete_inputs,
+            input_values,
+            prev_n,
+            n,
+            prune,
+            stride,
+            &smt_solver,
+            timeout,
+            minimize,
+            terminate_on_bad,
+            one_query
+        );
+
+        exec_time += elapsed;
+
+        if has_time_budget && time_budget.unwrap() < exec_time {
+            exec_time -= elapsed;
+
+            debug!("Time budget exceeded: {:#?} ({:#?}+{:#?}; elapsed time) / {:#?} (time budget)", exec_time+elapsed, exec_time, elapsed, time_budget.unwrap());
+
+            // TODO(2): Cf. TODO(1)
+            let r = reason_backwards(
+                &mut model.clone(),
+                &bad_states_initial,
+                prev_n,
+                n,
+                prune,
+                stride,
+                &smt_solver,
+                timeout,
+                minimize,
+                terminate_on_bad,
+                one_query,
+                &mut(time_budget.unwrap() - exec_time)
+            );
+
+            warn!("Reasoning horizon: depth [n={}] in {:#?} (elapsed time) / {:#?} (time budget)", prev_n + r.0, exec_time + r.1, time_budget.unwrap());
+            break;
+        }
+
+        if !stride || !model.bad_states_initial.is_empty() {
+            if !model.bad_states_initial.is_empty() {
+                print_reasoning_horizon(model);
+            }
+
+            break;
+        }
+
+        if has_time_budget {
+            debug!("Remaining time budget: {:#?} ...", time_budget.unwrap() - exec_time);
+        }
+
+        prev_n = n;
+        n = min(2*n, unroll_depth);
+    }
+}
+
+pub fn reason(
+    model: &mut Model,
+    has_concrete_inputs: bool,
+    input_values: &mut Vec<u64>,
+    start: usize,
+    end: usize,
+    prune: bool,
+    stride: bool,
+    smt_solver: &SmtType,
+    timeout: Option<Duration>,
+    minimize: bool,
+    terminate_on_bad: bool,
+    one_query: bool
+) -> (Duration, Vec<NodeRef>) {
+    let now = Instant::now();
+
+    for m in start..end {
+        unroll_model(model, m);
+
+        if has_concrete_inputs {
+            optimize_model_with_input(model, input_values)
+        }
+    }
+
+    if prune {
+        prune_model(model);
+    }
+
+    let bad_states_initial = model.bad_states_initial.clone();
+
+    match smt_solver {
+        #[rustfmt::skip]
+        SmtType::Generic => {
+            optimize_model_with_solver::<none_impl::NoneSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+        #[rustfmt::skip]
+        #[cfg(feature = "boolector")]
+        SmtType::Boolector => {
+            optimize_model_with_solver::<boolector_impl::BoolectorSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+        #[rustfmt::skip]
+        #[cfg(feature = "z3")]
+        SmtType::Z3 => {
+            optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+        },
+    }
+
+    (now.elapsed(), bad_states_initial)
+}
+
+//
+// Private Interface
+//
+
+fn reason_backwards(
+  model: &mut Model,
+  bad_states_initial: &Vec<NodeRef>,
+  prev_n: usize,
+  n: usize,
+  prune: bool,
+  stride: bool,
+  smt_solver: &SmtType,
+  timeout: Option<Duration>,
+  minimize: bool,
+  terminate_on_bad: bool,
+  one_query: bool,
+  time_budget: &mut Duration,
+) -> (usize, Duration) {
+  debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len());
+
+  if prune {
+      prune_model(model)
+  }
+
+  let mut start: usize = 0;
+  let mut end: usize = n - prev_n;
+  
+  let mut exec_n: usize = end;
+  let mut exec_time = Duration::from_millis(0);
+
+  let mut mid: usize = start + (end - start) / 2;
+  let mut prev_mid: usize;
+
+  while start < end {
+      debug!("Trying to fit remaining time budget {:#?} into the last {} steps ({} to {}) ...", time_budget, mid, mid, end);
+      
+      let now = Instant::now();
+
+      model.bad_states_initial =
+          bad_states_initial.clone()[mid * 10 .. end * 10].to_vec();
+
+      match smt_solver {
+          #[rustfmt::skip]
+          SmtType::Generic => {
+              optimize_model_with_solver::<none_impl::NoneSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+          #[rustfmt::skip]
+          #[cfg(feature = "boolector")]
+          SmtType::Boolector => {
+              optimize_model_with_solver::<boolector_impl::BoolectorSolver>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+          #[rustfmt::skip]
+          #[cfg(feature = "z3")]
+          SmtType::Z3 => {
+              optimize_model_with_solver::<z3solver_impl::Z3SolverWrapper>(model, timeout, minimize, terminate_on_bad, one_query, stride)
+          },
+      }
+
+      let elapsed = now.elapsed();
+      
+      if *time_budget > elapsed {
+        end = mid;
+        
+        exec_time += elapsed;
+          *time_budget -= elapsed;
+
+          debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed);
+      } else if *time_budget < elapsed {
+          start = mid;
+
+          exec_n = mid;
+          exec_time = elapsed;
+        
+          debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed);
+      }
+
+      // since we will not find a perfectly fitting time budget (as is the case
+      // in a traditional binary search), we need an additional termination
+      // criterion to avoid endless loops:
+      // We terminate once the pivot does not change anymore.
+      prev_mid = mid;
+      mid = start + (end - start)/2;
+
+      if prev_mid == mid {
+          break;
+      }
+
+  }
+
+  (exec_n, exec_time)
+}
+
+fn print_reasoning_horizon(model: &mut Model) {
+    let v: Option<String>;
+    v = match &*model.bad_states_initial[0].borrow() {
+        Node::Bad { name, ..} => name.clone(),
+        _ => None
+    };
+    
+    let bad_state = v.as_ref().expect("Bad state must have an unrolling depth");
+    warn!("(Initial) Bad state '{}' is satisfiable.", bad_state);
+}
\ No newline at end of file
diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs
index e31e3ff2..0a3cb45d 100644
--- a/src/unicorn/mod.rs
+++ b/src/unicorn/mod.rs
@@ -24,6 +24,7 @@ pub mod qubot;
 pub mod sat_solver;
 pub mod smt_solver;
 pub mod unroller;
+pub mod horizon;
 
 pub type Nid = u64;
 pub type NodeRef = Rc<RefCell<Node>>;
@@ -182,7 +183,7 @@ pub fn get_nodetype(n: usize) -> NodeType {
     }
 }
 
-#[derive(Debug)]
+#[derive(Clone, Debug)]
 pub struct Model {
     pub lines: Vec<NodeRef>,
     pub sequentials: Vec<NodeRef>,
diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs
index 5cf946b2..d42ef112 100644
--- a/src/unicorn/optimize.rs
+++ b/src/unicorn/optimize.rs
@@ -18,6 +18,7 @@ pub fn optimize_model_with_solver<S: SMTSolver>(
     minimize: bool,
     terminate_on_bad: bool,
     one_query: bool,
+    stride: bool
 ) {
     debug!("Optimizing model using '{}' SMT solver ...", S::name());
     debug!("Setting SMT solver timeout to {:?} per query ...", timeout);
@@ -29,12 +30,13 @@ pub fn optimize_model_with_solver<S: SMTSolver>(
         minimize,
         terminate_on_bad,
         one_query,
+        stride
     )
 }
 
 pub fn optimize_model_with_input(model: &mut Model, inputs: &mut Vec<u64>) {
     debug!("Optimizing model with {} concrete inputs ...", inputs.len());
-    optimize_model_impl::<none_impl::NoneSolver>(model, inputs, None, false, false, false);
+    optimize_model_impl::<none_impl::NoneSolver>(model, inputs, None, false, false, false, false);
 }
 
 //
@@ -48,6 +50,7 @@ fn optimize_model_impl<S: SMTSolver>(
     minimize: bool,
     terminate_on_bad: bool,
     one_query: bool,
+    stride: bool
 ) {
     let mut constant_folder = ConstantFolder::<S>::new(inputs, timeout, minimize);
     model
@@ -70,10 +73,15 @@ fn optimize_model_impl<S: SMTSolver>(
             .retain(|s| constant_folder.should_retain_bad_state(s, false, true));
 
         if model.bad_states_initial.is_empty() {
-            panic!("No bad states happen");
+            if !stride {
+                panic!("No bad states happen");
+            }
         } else if model.bad_states_initial.len() == 1 {
             constant_folder.should_retain_bad_state(&model.bad_states_initial[0], true, true);
-            panic!("No bad states happen");
+
+            if !stride {
+                panic!("No bad states happen");
+            }
         } else {
             let mut ored_bad_states = NodeRef::from(Node::Or {
                 nid: u64::MAX,
@@ -91,9 +99,13 @@ fn optimize_model_impl<S: SMTSolver>(
                 });
             }
             if !constant_folder.smt_solver.is_always_false(&ored_bad_states) {
-                panic!("bad states are satisfiable!")
+                if !stride {
+                    panic!("bad states are satisfiable!")
+                }
             } else {
-                panic!("No bad state happen.")
+                if !stride {
+                    panic!("No bad state happen.")
+                }
             }
         }
     }
@@ -699,7 +711,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> {
         if let Node::Bad { cond, name, .. } = &*bad_state.borrow() {
             if is_const_false(cond) {
                 debug!(
-                    "Bad state '{}' became unreachable, removing",
+                    "Bad state '{}' became statically unreachable, removing",
                     name.as_deref().unwrap_or("?")
                 );
                 return false;
diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs
index ca4c2767..29dff667 100644
--- a/src/unicorn/smt_solver.rs
+++ b/src/unicorn/smt_solver.rs
@@ -20,6 +20,7 @@ pub trait SMTSolver {
     fn new(timeout: Option<Duration>) -> Self;
     fn name() -> &'static str;
     fn solve(&mut self, root: &NodeRef) -> SMTSolution;
+    fn solve_n(&mut self, nodes: &Vec<NodeRef>) -> SMTSolution;
     fn is_always_true(&mut self, node: &NodeRef) -> bool;
     fn is_always_false(&mut self, node: &NodeRef) -> bool;
     fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool;
@@ -61,6 +62,10 @@ pub mod none_impl {
         fn solve(&mut self, _root: &NodeRef) -> SMTSolution {
             SMTSolution::Timeout
         }
+
+        fn solve_n(&mut self, _nodes: &Vec<NodeRef>) -> SMTSolution {
+          SMTSolution::Timeout
+        }
     }
 }
 
@@ -131,6 +136,14 @@ pub mod boolector_impl {
             let bv = self.visit(root).into_bv();
             self.solve_impl(bv.slice(0, 0))
         }
+
+        fn solve_n(&mut self, nodes: &Vec<NodeRef>) -> SMTSolution {
+          let bv = BV::zero(self.solver.clone(), 1);
+          for node in nodes.iter() {
+            bv.or(&self.visit(node).into_bv());
+          }
+          self.solve_impl(bv)
+        }
     }
 
     impl BoolectorSolver {
@@ -362,6 +375,10 @@ pub mod z3solver_impl {
             let z3_bool = self.visit(root).as_bool().expect("bool");
             self.solve_impl(&z3_bool)
         }
+
+        fn solve_n(&mut self, _nodes: &Vec<NodeRef>) -> SMTSolution {
+          SMTSolution::Timeout
+        }
     }
 
     impl<'ctx> Z3SolverWrapper<'ctx> {