Enable CBMC's equation-level slicer (rust-lang#1252)

celinval · Jun 8, 2022 · 7c6ad14 · 7c6ad14
1 parent 5d206d6
commit 7c6ad14
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -91,6 +91,8 @@ impl KaniSession {
             args.push(unwind_value.to_string().into());
         }
 
+        args.push("--slice-formula".into());
+
         args.extend(self.args.cbmc_args.iter().cloned());
 
         args.push(file.to_owned().into_os_string());