diff --git a/examples/eq.rs b/examples/eq.rs
index b4e36a8689287e78da514e07b7d08858f99907a6..ae2a410025fd9a023484e60018e40b2db19aae5e 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -30,13 +30,14 @@ const F: bool = false;
 
 #[no_mangle]
 fn main() {
-    let mut DATA: [Data; (DISCREPENCY + 2) as usize] = unsafe { core::mem::uninitialized() };
+    let mut DATA: [Data; (DISCREPENCY + 2) as usize] =
+        unsafe { core::mem::uninitialized() };
     ksymbol!(&mut DATA, "DATA");
 
     let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
         unsafe { core::mem::uninitialized() };
 
-    let mut TIMEOUT_CNTR: u32 = DISCREPENCY;
+    let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
     let mut STATE = S8001;
 
     for i in 0..(DISCREPENCY + 2) as usize {
@@ -62,66 +63,73 @@ fn main() {
         }
 
         // S8001 -> !a & !b
-        // we can only stay or enter the Init state if both inputs are false
+        // we can only stay or enter the Init state if either input are false
         if STATE == S8001 {
-            kassert!(TIMEOUT_CNTR == DISCREPENCY);
+            // kassert!(TIMEOUT_CNTR == DISCREPENCY);
             kassert!(!DATA[i].a | !DATA[i].b);
         }
 
-        // !a & !b & !timeout-> S8001
-        // ensures that we enter the Init state if both inputs are false
-        // under the condition that a timout has not occured
-        if !DATA[i].a & !DATA[i].b & (TIMEOUT_CNTR > 0) {
-            kassert!(STATE == S8001);
-        }
-
-        // DISCREPANCY related invariants
-        match STATE {
-            // Error -> timeout
-            // error states implies TIMEOUT_CNTR to have expired
-            C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
-            // Waiting states -> !timeout
-            // wait states implies that TIMEOUT_CNTR not yet expired
-            // and that the time remaining is not longer than the discrepency
-            S8004 | S8005 | S8014 => kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY),
-            _ => {}
-        }
-
-        // transition invariants
-        if i > 0 {
-            match STATE_HISTORY[i - 1] {
-                C001 | C002 | C003 | S8005 => {
-                    //
-                    // no (immediate) transition from error / recover to Enable state
-                    kassert!(!(STATE == S8000));
-                }
-                _ => {
-                    // liveness from Init and Wait states, Enable is ensured
-                    if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
-                        kassert!(STATE == S8000);
-                    }
-                }
-            }
-        }
+        // // !a & !b & !timeout-> S8001
+        // // ensures that we enter the Init state if both inputs are false
+        // // under the condition that a timout has not occured
+        // if !DATA[i].a & !DATA[i].b {
+        //     kassert!(STATE == S8001);
+        // }
+
+        // // DISCREPANCY related invariants
+        // match STATE {
+        //     // Error -> timeout
+        //     // error states implies TIMEOUT_CNTR to have expired
+        //     C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+        //     // Waiting states -> !timeout
+        //     // wait states implies that TIMEOUT_CNTR not yet expired
+        //     // and that the time remaining is not longer than the discrepency
+        //     S8004 | S8005 | S8014 => {
+        //         kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
+        //     }
+        //     _ => {}
+        // }
+
+        // // transition invariants
+        // if i > 0 {
+        //     match STATE_HISTORY[i - 1] {
+        //         C001 | C002 | C003 | S8005 => {
+        //             //
+        //             // no (immediate) transition from error / recover to Enable state
+        //             kassert!(!(STATE == S8000));
+        //         }
+        //         _ => {
+        //             // liveness from Init and Wait states, Enable is ensured
+        //             if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
+        //                 kassert!(STATE == S8000);
+        //             }
+        //         }
+        //     }
+        // }
         STATE_HISTORY[i] = STATE;
     }
 }
 
 fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
-
     *STATE = match STATE {
         S8000 => match (data.a, data.b) {
-            (F, F) => {
+            (F, F) => S8001,
+            (F, T) | (T, F) => {
                 *TIMEOUT_CNTR = DISCREPENCY;
-                S8001
+                S8005
             }
-            (F, T) | (T, F) => S8005,
             (T, T) => S8000,
         },
         S8001 => match (data.a, data.b) {
             (F, F) => S8001,
-            (F, T) => S8014,
-            (T, F) => S8004,
+            (F, T) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8014
+            }
+            (T, F) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8004
+            }
             (T, T) => S8000,
         },
         S8004 => {
@@ -129,10 +137,7 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
             match *TIMEOUT_CNTR {
                 0 => C001,
                 _ => match (data.a, data.b) {
-                    (F, _) => {
-                        *TIMEOUT_CNTR = DISCREPENCY;
-                        S8001
-                    }
+                    (F, _) => S8001,
                     (_, T) => S8000,
                     _ => S8004,
                 },
@@ -143,10 +148,7 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
             match *TIMEOUT_CNTR {
                 0 => C002,
                 _ => match (data.a, data.b) {
-                    (_, F) => {
-                        *TIMEOUT_CNTR = DISCREPENCY;
-                        S8001
-                    }
+                    (_, F) => S8001,
                     (T, _) => S8000,
                     _ => S8014,
                 },
@@ -157,26 +159,17 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
             match *TIMEOUT_CNTR {
                 0 => C003,
                 _ => match (data.a, data.b) {
-                    (F, F) => {
-                        *TIMEOUT_CNTR = DISCREPENCY;
-                        S8001
-                    }
+                    (F, F) => S8001,
                     _ => S8005,
                 },
             }
         }
         C001 | C002 => match (data.a, data.b) {
-            (F, F) => {
-                *TIMEOUT_CNTR = DISCREPENCY;
-                S8001
-            }
+            (F, F) => S8001,
             _ => *STATE,
         },
         C003 => match (data.a, data.b) {
-            (F, F) => {
-                *TIMEOUT_CNTR = DISCREPENCY;
-                S8001
-            }
+            (F, F) => S8001,
             _ => C003,
         },
     };