diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
new file mode 100644
index 0000000000000000000000000000000000000000..a881738d0cda0d7333d0a572b54b25425c3f4118
--- /dev/null
+++ b/examples/eq_paper.rs
@@ -0,0 +1,202 @@
+#![allow(non_snake_case)]
+#![no_main]
+
+extern crate klee;
+use klee::{kassert, kassume, ksymbol};
+
+#[derive(Debug, Copy, Clone)]
+pub struct Data {
+  a: bool,
+  b: bool,
+}
+
+#[derive(Debug, Copy, Clone, PartialEq)]
+pub enum State {
+  S8000,
+  S8001,
+  S8004,
+  S8014,
+  S8005,
+  C001,
+  C002,
+  C003,
+}
+
+use State::*;
+
+const DISCREPANCY: u32 = 1;
+const HORIZON: usize = (DISCREPANCY + 4) as usize;
+const T: bool = true;
+const F: bool = false;
+
+#[no_mangle]
+fn main() {
+  let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
+  ksymbol!(&mut DATA, "DATA");
+
+  let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
+
+  let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
+
+  let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+  let mut STATE = S8001;
+
+  for i in 0..HORIZON {
+    periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+    STATE_H[i] = STATE;
+    CNTR_H[i] = TIMEOUT_CNTR;
+
+    // invariants
+    // S8000 -> a & b
+    // ensures that Enable implies that both a and b are true
+    // this is the main safety condition
+    if STATE == S8000 {
+      kassert!(DATA[i].a & DATA[i].b);
+    }
+
+    // !a | !b -> !S8000
+    // ensures that if any input is false we cannot enter the Enable state
+    // this can also be seen as a safty condition
+    // (can it be derived from the first condition, but we keep is as
+    // an indication that the verification works as expected)
+    // Indeed the number of spanned paths remains the same
+    // (with or without the below assertion, so its proven redundant by KLEE)
+    if !DATA[i].a | !DATA[i].b {
+      kassert!(!(STATE == S8000));
+    }
+
+    // S8001 -> !a & !b
+    // we can only stay or enter the Init state unless either (or both) inputs are false
+    if STATE == S8001 {
+      kassert!(!DATA[i].a | !DATA[i].b);
+    }
+
+    // transition invariants
+    if i > 0 {
+      match STATE_H[i - 1] {
+        C001 | C002 | C003 => {
+          // transitions from error
+          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+        }
+        S8005 => {
+          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+        }
+        _ => (),
+      }
+    }
+
+    // // DISCREPANCY related invariants
+    match STATE {
+      // Error -> timeout
+      C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+
+      S8004 | S8005 | S8014 => {
+        // // remaining in a waiting state decreases the counter
+        if i > 0 {
+          if STATE_H[i - 1] == STATE_H[i] {
+            kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
+          }
+        }
+        // // Waiting states -> !timeout
+        // // Waiting states implies that TIMEOUT_CNTR has not yet expired
+        // // and that the time remaining is not longer than the DISCREPANCY
+        //   kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+        // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
+      }
+      _ => {}
+    }
+
+    // // liveness?
+    // if i == HORIZON - 1 {
+    //   let mut ok = false;
+    //   for j in 0..=i {
+    //     if STATE_H[j] == S8001 {
+    //       ok = true;
+    //     }
+    //   }
+    //   kassert!(ok);
+    // }
+
+    // if i > 0 {
+    //   match STATE_H[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);
+    //       }
+    //     }
+    //   }
+    // }
+
+    unsafe { core::ptr::read_volatile(&STATE_H[i]) };
+  }
+}
+
+fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+  *STATE = match STATE {
+    S8000 => match (data.a, data.b) {
+      (F, F) => S8001,
+      (F, T) | (T, F) => {
+        *TIMEOUT_CNTR = DISCREPANCY;
+        S8005
+      }
+      (T, T) => S8000,
+    },
+    S8001 => match (data.a, data.b) {
+      (F, F) => S8001,
+      (F, T) => {
+        *TIMEOUT_CNTR = DISCREPANCY;
+        S8014
+      }
+      (T, F) => {
+        *TIMEOUT_CNTR = DISCREPANCY;
+        S8004
+      }
+      (T, T) => S8000,
+    },
+    S8004 => match *TIMEOUT_CNTR {
+      0 => C001,
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
+          (F, _) => S8001,
+          (_, T) => S8000,
+          _ => S8004,
+        }
+      }
+    },
+    S8014 => match *TIMEOUT_CNTR {
+      0 => C002,
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
+          (_, F) => S8001,
+          (T, _) => S8000,
+          _ => S8014,
+        }
+      }
+    },
+    S8005 => match *TIMEOUT_CNTR {
+      0 => C003,
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
+          (F, F) => S8001,
+          _ => S8005,
+        }
+      }
+    },
+    C001 | C002 => match (data.a, data.b) {
+      (F, F) => S8001,
+      _ => *STATE,
+    },
+    C003 => match (data.a, data.b) {
+      (F, F) => S8001,
+      _ => C003,
+    },
+  };
+}