fix: Use absolute depth during unrolling and simplify print_reasoning…

…_horizon

src/main.rs

@@ -118,15 +118,16 @@ fn main() -> Result<()> {
 
                     let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms));
 
-                    let mut n: usize = if stride { 1 } else { unroll_depth };
+                    let mut n: usize = if stride { 0 } else { unroll_depth };
+                    let mut prev_n: usize = 0;
                     loop {
                         // TODO: 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 mut model_copy = model.clone();
 
-                        for m in 0..n {
+                        for m in prev_n..n {
                             unroll_model(&mut model_copy, m);
 
                             if has_concrete_inputs {
@@ -135,7 +136,7 @@ fn main() -> Result<()> {
                         }
 
                         if prune {
-                          prune_model(&mut model_copy);
+                            prune_model(&mut model_copy);
                         }
 
                         match smt_solver {
@@ -157,13 +158,14 @@ fn main() -> Result<()> {
 
                         if !stride || !model_copy.bad_states_initial.is_empty() {
                             if !model_copy.bad_states_initial.is_empty() {
-                              print_reasoning_horizon(&mut model_copy, n, stride);
+                                print_reasoning_horizon(&mut model_copy);
                             }
 
                             break;
                         }
 
-                        n = min(2 * n, unroll_depth);
+                        prev_n = n;
+                        n = min(2*n, unroll_depth);
                     }
 
                     if renumber {

src/unicorn/horizon.rs

@@ -5,22 +5,13 @@ use log::warn;
 // Public Interface
 //
 
-pub fn print_reasoning_horizon(model: &mut Model, depth: usize, stride: bool) {
+pub 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 ss = v.as_ref().expect("Bad state must have an unrolling depth");
-    if let (Some(start), Some(end)) = (ss.find("[n="), ss.find("]")) {
-        if let (reason, Ok(remainder)) = (ss[..start].to_string(), ss[start+"[n=".len()..end].to_string().parse::<usize>()) {
-            warn!(
-                "(Initial) Bad state '{}[n={:#?}]' is satisfiable.",
-                reason,
-                if stride { (depth - 1) + remainder } else { remainder }
-            );
-        }
 
-    }
+    let bad_state = v.as_ref().expect("Bad state must have an unrolling depth");
+    warn!("(Initial) Bad state '{}' is satisfiable.", bad_state);
 }