works again

Cargo.toml

@@ -36,6 +36,7 @@ incremental = false
 [profile.release]
 debug = true
 panic = "abort"
+incremental = false
 lto = true
 
 [features]

examples/eq.rs

@@ -4,10 +4,33 @@
 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 DISCREPENCY: u32 = 3;
+const T: bool = true;
+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] =
@@ -41,7 +64,8 @@ fn main() {
         // S8001 -> !a & !b
         // we can only stay or enter the Init state if both inputs are false
         if STATE == S8001 {
-            kassert!(TIMEOUT_CNTR == DISCREPENCY && !DATA[i].a | !DATA[i].b);
+            kassert!(TIMEOUT_CNTR == DISCREPENCY);
+            kassert!(!DATA[i].a | !DATA[i].b);
         }
 
         // !a & !b & !timeout-> S8001
@@ -51,7 +75,7 @@ fn main() {
             kassert!(STATE == S8001);
         }
 
-        // DISCREPANCY relatod invariants
+        // DISCREPANCY related invariants
         match STATE {
             // Error -> timeout
             // error states implies TIMEOUT_CNTR to have expired
@@ -59,9 +83,7 @@ fn main() {
             // 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)
-            }
+            S8004 | S8005 | S8014 => kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY),
             _ => {}
         }
 
@@ -85,56 +107,21 @@ fn main() {
     }
 }
 
-#[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 DISCREPENCY: u32 = 3;
-const T: bool = true;
-const F: bool = false;
-
-fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
-    // we start directly in the init state S80001
-    // static mut STATE: State = State::S8001;
-    // static mut TIMEOUT_CNTR: u32 = 0;
-
-    let data = DATA;
+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) => {
+            (F, F) => {
                 *TIMEOUT_CNTR = DISCREPENCY;
-                S8005
+                S8001
             }
+            (F, T) | (T, F) => S8005,
             (T, T) => S8000,
         },
         S8001 => match (data.a, data.b) {
             (F, F) => S8001,
-            (F, T) => {
-                *TIMEOUT_CNTR = DISCREPENCY;
-                S8014
-            }
-            (T, F) => {
-                *TIMEOUT_CNTR = DISCREPENCY;
-                S8004
-            }
+            (F, T) => S8014,
+            (T, F) => S8004,
             (T, T) => S8000,
         },
         S8004 => {
@@ -142,7 +129,10 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
             match *TIMEOUT_CNTR {
                 0 => C001,
                 _ => match (data.a, data.b) {
-                    (F, _) => S8001,
+                    (F, _) => {
+                        *TIMEOUT_CNTR = DISCREPENCY;
+                        S8001
+                    }
                     (_, T) => S8000,
                     _ => S8004,
                 },
@@ -153,7 +143,10 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
             match *TIMEOUT_CNTR {
                 0 => C002,
                 _ => match (data.a, data.b) {
-                    (_, F) => S8001,
+                    (_, F) => {
+                        *TIMEOUT_CNTR = DISCREPENCY;
+                        S8001
+                    }
                     (T, _) => S8000,
                     _ => S8014,
                 },
@@ -164,17 +157,26 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
             match *TIMEOUT_CNTR {
                 0 => C003,
                 _ => match (data.a, data.b) {
-                    (F, F) => S8001,
+                    (F, F) => {
+                        *TIMEOUT_CNTR = DISCREPENCY;
+                        S8001
+                    }
                     _ => S8005,
                 },
             }
         }
         C001 | C002 => match (data.a, data.b) {
-            (F, F) => S8001,
+            (F, F) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8001
+            }
             _ => *STATE,
         },
         C003 => match (data.a, data.b) {
-            (F, F) => S8001,
+            (F, F) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8001
+            }
             _ => C003,
         },
     };