diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml
new file mode 100644
index 000000000000..e9f973c82919
--- /dev/null
+++ b/.github/workflows/kani-m1.yml
@@ -0,0 +1,30 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Run the regression job on Apple M1 only on commits to `main`
+name: Kani CI M1
+on:
+  push:
+    branches:
+      - 'main'
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  regression:
+    runs-on: macos-13-xlarge
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v3
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-13-xlarge
+
+      - name: Build Kani
+        run: cargo build-dev
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh
diff --git a/kani-dependencies b/kani-dependencies
index 9b86df41cc16..200755839284 100644
--- a/kani-dependencies
+++ b/kani-dependencies
@@ -1,6 +1,6 @@
 CBMC_MAJOR="5"
-CBMC_MINOR="94"
-CBMC_VERSION="5.94.0"
+CBMC_MINOR="95"
+CBMC_VERSION="5.95.1"
 
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_MAJOR="3"
diff --git a/kani-driver/src/call_goto_synthesizer.rs b/kani-driver/src/call_goto_synthesizer.rs
index 277201cabb18..9853123dc29a 100644
--- a/kani-driver/src/call_goto_synthesizer.rs
+++ b/kani-driver/src/call_goto_synthesizer.rs
@@ -35,7 +35,18 @@ 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. and array-as-uninterpreted-functions options, which should be included
+        //    in the cbmc_args.
+        args.extend(self.args.cbmc_args.iter().cloned());
 
         let mut cmd = Command::new("goto-synthesizer");
         cmd.args(args);
diff --git a/scripts/setup/macos-13-xlarge b/scripts/setup/macos-13-xlarge
new file mode 120000
index 000000000000..a8d0f9c4854d
--- /dev/null
+++ b/scripts/setup/macos-13-xlarge
@@ -0,0 +1 @@
+macos
\ No newline at end of file
diff --git a/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
index f981ca8fa12b..3a1302111b32 100644
--- a/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
+++ b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --enable-unstable --synthesize-loop-contracts
+// kani-flags: --enable-unstable --synthesize-loop-contracts --cbmc-args --object-bits 4
 
 // Check if goto-synthesizer is correctly called, and synthesizes the required
 // loop invariants.