Propogate backend options into goto-synthesizer

model-checking · Jul 30, 2023 · 82bc123 · 82bc123
1 parent f024d23
commit 82bc123
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/kani-driver/src/call_goto_synthesizer.rs b/kani-driver/src/call_goto_synthesizer.rs
@@ -35,7 +35,21 @@ impl KaniSession {
             output.to_owned().into_os_string(), // output
         ];
 
+        // goto-synthesizer should take the same backend options as cbmc.
+        // Backend options include
+        // 1. solver options
         self.handle_solver_args(&harness_metadata.attributes.solver, &mut args)?;
+        // 2. object-bits option
+        if let Some(object_bits) = self.args.cbmc_object_bits() {
+            args.push("--object-bits".into());
+            args.push(object_bits.to_string().into());
+        }
+        // 3. array-as-uninterpreted-functions options
+        if self.args.cbmc_args.contains(&OsString::from("--arrays-uf-always")) {
+            args.push("--arrays-uf-always".into());
+        } else if self.args.cbmc_args.contains(&OsString::from("--arrays-uf-never")) {
+            args.push("--arrays-uf-never".into());
+        }
 
         let mut cmd = Command::new("goto-synthesizer");
         cmd.args(args);