diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
index fcccef2190b211b9cea82f87c570e2b63334eb5c..5c0c70ccd481e0a2acbe37e5b1aed58e552e9069 100644
--- a/examples/eq_dfs.rs
+++ b/examples/eq_dfs.rs
@@ -142,11 +142,10 @@ fn main() {
     //   }
     // }
 
-
     let mut is_visited = false;
     match STATE {
       S8004 | S8005 | S8014 => {
-          for j in 0..i {
+        for j in 0..i {
           if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
             is_visited = true;
           }
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 9eeeb2a3b8cace229a3c982f296307434e2fa471..ad1ffd03bcfc6ac927eabd8d4d3a4ad910fc4ae6 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -2,9 +2,8 @@
 #![no_main]
 #![no_std]
 
-
-extern crate panic_abort;
 extern crate klee;
+extern crate panic_abort;
 use klee::{kassert, kassume, ksymbol};
 
 #[derive(Debug, Copy, Clone)]
@@ -40,6 +39,7 @@ fn main() {
   let mut STATE = S8001;
   let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() }; // STATE_HISTORY
   let mut CNTR: u32 = unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
+
   // TIMEOUT_CNTR_HISTORY
   let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
 
@@ -53,28 +53,21 @@ fn main() {
     if !DATA[i].a | !DATA[i].b {
       kassert!(!(STATE == S8000));
     }
-    
+
     // (2) S8000 -> a & b
     if STATE == S8000 {
       kassert!(DATA[i].a & DATA[i].b);
     }
-    
+
     if i > 0 {
       match STATE_H[i - 1] {
         // (3)
         C001 | C002 | C003 => {
-          kassert!(
-              (STATE == S8001) 
-            | (STATE == STATE_H[i - 1])
-          );
+          kassert!((STATE == S8001) | (STATE == STATE_H[i - 1]));
         }
         // (4)
         S8005 => {
-          kassert!(
-            (STATE == S8001) 
-          | (STATE == C003) 
-          | (STATE == STATE_H[i - 1])
-          );
+          kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
         }
         _ => (),
       }
@@ -97,7 +90,11 @@ fn main() {
   }
 }
 
-fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+fn eq(
+  STATE: &mut State,
+  TIMEOUT_CNTR: &mut u32,
+  data: &Data,
+) {
   *STATE = match STATE {
     S8000 => match (data.a, data.b) {
       (F, F) => S8001,