diff --git a/examples/concurrent.rs b/examples/concurrent.rs
index 000bcab7a94c4ee04dc5f339794c4a3f7c1835ae..81229d7bdabc44200060b58b0807ef67b0ca3777 100644
--- a/examples/concurrent.rs
+++ b/examples/concurrent.rs
@@ -11,9 +11,12 @@ use volatile_register::{RO, RW, WO};
 
 #[no_mangle]
 fn main() {
-  let rw: RW<u32> = unsafe { core::mem::uninitialized() };
-  let ro: RO<u32> = unsafe { core::mem::uninitialized() };
-  let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+  let rw: RW<u32> =
+    unsafe { core::mem::uninitialized() };
+  let ro: RO<u32> =
+    unsafe { core::mem::uninitialized() };
+  let wo: WO<u32> =
+    unsafe { core::mem::uninitialized() };
 
   unsafe { wo.write(2) };
 
diff --git a/examples/eq.rs b/examples/eq.rs
index 59600a57a92b97974bb95470e0231a5ff2220662..50f7e7cb6b7e9e3de867723f80fe87b479c57486 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -31,18 +31,26 @@ const F: bool = false;
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
+  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 STATE_H: [State; HORIZON] =
+    unsafe { core::mem::uninitialized() };
 
-  let mut CNTR_H: [u32; 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 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]);
+    periodic(
+      &mut STATE,
+      &mut TIMEOUT_CNTR,
+      &mut DATA[i],
+    );
     STATE_H[i] = STATE;
     CNTR_H[i] = TIMEOUT_CNTR;
 
@@ -76,10 +84,17 @@ fn main() {
       match STATE_H[i - 1] {
         C001 | C002 | C003 => {
           // transitions from error
-          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+          kassert!(
+            (STATE_H[i] == S8001)
+              | (STATE == STATE_H[i - 1])
+          );
         }
         S8005 => {
-          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+          kassert!(
+            (STATE_H[i] == S8001)
+              | (STATE == C003)
+              | (STATE == STATE_H[i - 1])
+          );
         }
         _ => (),
       }
diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
index 5c0c70ccd481e0a2acbe37e5b1aed58e552e9069..5a372b8bc3aa7e7ea8a9892fb3b97efdf983e0c9 100644
--- a/examples/eq_dfs.rs
+++ b/examples/eq_dfs.rs
@@ -35,14 +35,18 @@ const F: bool = false;
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; HORIZON + 1] =
+    unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-  let mut STATE_H: [State; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+  let mut STATE_H: [State; HORIZON + 1] =
+    unsafe { core::mem::uninitialized() };
 
-  let mut CNTR_H: [u32; HORIZON + 1] = unsafe { core::mem::uninitialized() };
+  let mut CNTR_H: [u32; HORIZON + 1] =
+    unsafe { core::mem::uninitialized() };
 
-  let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+  let mut TIMEOUT_CNTR: u32 =
+    unsafe { core::mem::uninitialized() };
   // initial state, Init
   let mut i = 0;
   let mut TIMEOUT_CNTR: u32 = DISCREPANCY;
@@ -86,10 +90,17 @@ fn main() {
       match STATE_H[i - 1] {
         C001 | C002 | C003 => {
           // transitions from error
-          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+          kassert!(
+            (STATE_H[i] == S8001)
+              | (STATE == STATE_H[i - 1])
+          );
         }
         S8005 => {
-          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+          kassert!(
+            (STATE_H[i] == S8001)
+              | (STATE == C003)
+              | (STATE == STATE_H[i - 1])
+          );
         }
         _ => (),
       }
@@ -146,7 +157,9 @@ fn main() {
     match STATE {
       S8004 | S8005 | S8014 => {
         for j in 0..i {
-          if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
+          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 ad1ffd03bcfc6ac927eabd8d4d3a4ad910fc4ae6..8449c50e9b6291694e9d1f12a6b0b407e97e9e69 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -33,15 +33,19 @@ const F: bool = false;
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; HORIZON] =
+    unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
   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
+  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() };
+  let mut CNTR_H: [u32; HORIZON] =
+    unsafe { core::mem::uninitialized() };
 
   for i in 0..HORIZON {
     eq(&mut STATE, &mut CNTR, &mut DATA[i]);
@@ -63,11 +67,18 @@ fn main() {
       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])
+          );
         }
         _ => (),
       }
diff --git a/examples/model2.rs b/examples/model2.rs
index b3842f029c6bfdb1d1508162c1e0736f34e8b604..1155ac33d46e040642c44b0f7916ed335081db65 100644
--- a/examples/model2.rs
+++ b/examples/model2.rs
@@ -50,8 +50,10 @@ impl RegB {
 
 #[no_mangle]
 fn main() {
-  let reg_a: RegA = unsafe { core::mem::uninitialized() };
-  let reg_b: RegB = unsafe { core::mem::uninitialized() };
+  let reg_a: RegA =
+    unsafe { core::mem::uninitialized() };
+  let reg_b: RegB =
+    unsafe { core::mem::uninitialized() };
 
   unsafe {
     reg_b.write(0);
diff --git a/examples/model3.rs b/examples/model3.rs
index ddea1f081d88a5e8c39fde53a4f4fbbb08f38701..8ca3db029d5491cb2e8fc6a1063ee9b4517a521c 100644
--- a/examples/model3.rs
+++ b/examples/model3.rs
@@ -38,8 +38,10 @@ impl RegC {
 
 #[no_mangle]
 fn main() {
-  let reg_c: RegC = unsafe { core::mem::uninitialized() };
-  let mut init: u32 = unsafe { core::mem::uninitialized() };
+  let reg_c: RegC =
+    unsafe { core::mem::uninitialized() };
+  let mut init: u32 =
+    unsafe { core::mem::uninitialized() };
   klee::ksymbol!(&mut init, "init");
   //klee::kassume(init < 0xFFFF_FFFC);
   //init = 0xFFFF_FFFD;
diff --git a/examples/model4.rs b/examples/model4.rs
index e1de24820c951f5ab69606845b191344afe0ad3f..3053828d72f26728bc42ff343f8d039d505f6ea1 100644
--- a/examples/model4.rs
+++ b/examples/model4.rs
@@ -37,8 +37,10 @@ impl RegC {
 
 #[no_mangle]
 fn main() {
-  let reg_c: RegC = unsafe { core::mem::uninitialized() };
-  let mut init: u32 = unsafe { core::mem::uninitialized() };
+  let reg_c: RegC =
+    unsafe { core::mem::uninitialized() };
+  let mut init: u32 =
+    unsafe { core::mem::uninitialized() };
   klee::ksymbol!(&mut init, "init");
   unsafe {
     reg_c.write(init); // to ensure that the initial value is symbolic
diff --git a/rustfmt.toml b/rustfmt.toml
index 1ddeb658d764278f694accb9ac0178ae0522e720..7d7193849591673efb0c229e95bf2c908691be43 100644
--- a/rustfmt.toml
+++ b/rustfmt.toml
@@ -1,2 +1,3 @@
 tab_spaces = 2
 fn_args_density = "Vertical"
+max_width = 56
diff --git a/src/main.rs b/src/main.rs
index 6f3432e1a3ea57d12b365415f45120f9a3fae4d0..f86a220a1211a4862d9e8f4c12a7e371d5b0eb2e 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -5,13 +5,16 @@ use klee::{kassert, ksymbol};
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; (DISCREPENCY + 1) as usize] =
+    unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-  let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+  let mut TIMEOUT_CNTR: u32 =
+    unsafe { core::mem::uninitialized() };
   ksymbol!(&mut TIMEOUT_CNTR, "TIMEOUT_CNTR");
 
-  let mut STATE_HISTORY: [State; (DISCREPENCY + 1) as usize] =
+  let mut STATE_HISTORY: [State;
+    (DISCREPENCY + 1) as usize] =
     unsafe { core::mem::uninitialized() };
 
   DATA[0] = Data { a: false, b: false };
@@ -19,7 +22,11 @@ fn main() {
   let mut STATE = S8001;
 
   for i in 0..(DISCREPENCY + 1) as usize {
-    periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+    periodic(
+      &mut STATE,
+      &mut TIMEOUT_CNTR,
+      &mut DATA[i as usize],
+    );
 
     // invariants
     // S8000 -> a & b