Add CI regression run for the write_goto_binary

Modified `call_single_file.rs` so that write_goto_binary
can be enabled by defining the KANI_ENABLE_WRITE_GOTO_BINARY
env variable.

.github/workflows/kani.yml

@@ -33,6 +33,25 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
+  write-goto-binary-regression:
+    runs-on: ubuntu-20.04
+    env:
+      KANI_ENABLE_WRITE_GOTO_BINARY: 1
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: ubuntu-20.04
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh
+
   experimental-features-regression:
     runs-on: ubuntu-20.04
     env:

kani-driver/src/call_single_file.rs

@@ -86,9 +86,19 @@ impl KaniSession {
         if self.args.ignore_global_asm {
             flags.push("--ignore-global-asm".into());
         }
-        if self.args.write_goto_binary {
+
+        // When running regression runs, the write_goto_binary option is enabled
+        // by defining an environment variable.
+        // The value must be non-empty and different from zero.
+        let enable_write_goto_binary = match std::env::var_os("KANI_ENABLE_WRITE_GOTO_BINARY") {
+            Some(str) => !str.is_empty() && str != "0",
+            None => false,
+        };
+        // Users activate it via the command line switch
+        if self.args.write_goto_binary || enable_write_goto_binary {
             flags.push("--write-goto-binary".into());
         }
+
         if self.args.enable_stubbing {
             flags.push("--enable-stubbing".into());
         }