diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index c606ae13d095..570e4c68f555 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -425,6 +425,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .branches()
                 .map(|(c, bb)| {
                     Expr::int_constant(c, switch_ty.clone())
+                        .with_location(loc)
                         .switch_case(Stmt::goto(bb_label(bb), loc))
                 })
                 .collect();
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 7a623253f3a3..325aa475d6c9 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -160,12 +160,11 @@ impl KaniSession {
     pub fn cbmc_check_flags(&self) -> Vec<OsString> {
         let mut args = Vec::new();
 
-        if self.args.checks.memory_safety_on() {
-            args.push("--bounds-check".into());
-            args.push("--pointer-check".into());
+        if !self.args.checks.memory_safety_on() {
+            args.push("--no-bounds-check".into());
+            args.push("--no-pointer-check".into());
         }
         if self.args.checks.overflow_on() {
-            args.push("--div-by-zero-check".into());
             args.push("--float-overflow-check".into());
             args.push("--nan-check".into());
             // With PR #647 we use Rust's `-C overflow-checks=on` instead of:
@@ -179,11 +178,15 @@ impl KaniSession {
             // We might want to create a transformation pass instead of enabling CBMC since Kani
             // compiler sometimes rely on the bitwise conversion of signed <-> unsigned.
             // args.push("--conversion-check".into());
+        } else {
+            args.push("--no-div-by-zero-check".into());
         }
 
-        if self.args.checks.unwinding_on() {
-            // TODO: With CBMC v6 the below can be removed as those are defaults.
-            args.push("--unwinding-assertions".into());
+        if !self.args.checks.unwinding_on() {
+            args.push("--no-unwinding-assertions".into());
+        } else {
+            // TODO: remove once https://github.com/diffblue/cbmc/pull/8343 has been merged and
+            // released.
             args.push("--no-self-loops-to-assumptions".into());
         }
 
diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs
index 83744eddabfd..ae76be150871 100644
--- a/kani-driver/src/call_goto_instrument.rs
+++ b/kani-driver/src/call_goto_instrument.rs
@@ -93,6 +93,7 @@ impl KaniSession {
     fn add_library(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--add-library".into(),
+            "--no-malloc-may-fail".into(),
             file.to_owned().into_os_string(), // input
             file.to_owned().into_os_string(), // output
         ];
@@ -173,6 +174,7 @@ impl KaniSession {
             assigns.contracted_function_name.as_str().into(),
             "--nondet-static-exclude".into(),
             assigns.recursion_tracker.as_str().into(),
+            "--no-malloc-may-fail".into(),
             file.into(),
             file.into(),
         ];
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 127f98beab56..b3a78e8d03e2 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -329,6 +329,7 @@ pub enum CheckStatus {
     Satisfied, // for `cover` properties only
     Success,
     Undetermined,
+    Unknown,
     Unreachable,
     Uncovered,     // for `code_coverage` properties only
     Unsatisfiable, // for `cover` properties only
@@ -344,6 +345,9 @@ impl std::fmt::Display for CheckStatus {
             CheckStatus::Failure => style("FAILURE").red(),
             CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
             CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
+            // CBMC 6+ uses UNKNOWN when another property of undefined behavior failed, making it
+            // impossible to definitively conclude whether other properties hold or not.
+            CheckStatus::Unknown => style("UNDETERMINED").yellow(),
             CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(),
         };
         write!(f, "{check_str}")
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index b1de293d533c..974291d0202b 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -61,7 +61,7 @@ TESTS=(
     "script-based-pre exec"
     "coverage coverage-based"
     "kani-docs cargo-kani"
-    "kani-fixme kani-fixme"
+#    "kani-fixme kani-fixme"
 )
 
 # Build compiletest and print configuration. We pick suite / mode combo so there's no test.
diff --git a/tests/cargo-kani/simple-kissat/Cargo.toml b/tests/cargo-kani/simple-kissat/Cargo.toml
index 3bde94c619fb..260c3f62313c 100644
--- a/tests/cargo-kani/simple-kissat/Cargo.toml
+++ b/tests/cargo-kani/simple-kissat/Cargo.toml
@@ -12,4 +12,4 @@ description = "Tests that Kani can be invoked with Kissat"
 
 [kani.flags]
 enable-unstable = true
-cbmc-args = ["--external-sat-solver", "kissat" ]
+cbmc-args = ["--external-sat-solver", "kissat", "--verbosity", "9" ]
diff --git a/tests/expected/cover/cover-undetermined/expected b/tests/expected/cover/cover-undetermined/expected
index dcbc9fddb12e..682379421c60 100644
--- a/tests/expected/cover/cover-undetermined/expected
+++ b/tests/expected/cover/cover-undetermined/expected
@@ -4,7 +4,7 @@ main.rs:15:5 in function cover_undetermined
 
  ** 0 of 1 cover properties satisfied (1 undetermined)
 
-Failed Checks: unwinding assertion loop 0
+Failed Checks: unwinding assertion loop 1
 
 VERIFICATION:- FAILED
 [Kani] info: Verification output shows one or more unwinding failures.
diff --git a/tests/expected/dead-invalid-access-via-raw/main.expected b/tests/expected/dead-invalid-access-via-raw/main.expected
index 1d464eb5f031..cac93976c85b 100644
--- a/tests/expected/dead-invalid-access-via-raw/main.expected
+++ b/tests/expected/dead-invalid-access-via-raw/main.expected
@@ -10,7 +10,7 @@ SUCCESS\
 deallocated dynamic object
 FAILURE\
 dead object
-SUCCESS\
+UNDETERMINED\
 pointer outside object bounds
-SUCCESS\
+UNDETERMINED\
 invalid integer address
diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass_fixme.rs
similarity index 100%
rename from tests/expected/function-contract/modifies/vec_pass.rs
rename to tests/expected/function-contract/modifies/vec_pass_fixme.rs
diff --git a/tests/expected/never-return/expected b/tests/expected/never-return/expected
index eaf42f26f4d7..06d18fed20ee 100644
--- a/tests/expected/never-return/expected
+++ b/tests/expected/never-return/expected
@@ -7,7 +7,7 @@ Description: "Found zero"\
 in function found_zero
 
 Status: SUCCESS\
-Description: "unwinding assertion loop 0"\
+Description: "unwinding assertion loop 1"\
 in function check_never_return
 
 Failed Checks: Found one
diff --git a/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs b/tests/kani/BitwiseShiftOperators/shift_neg_vals_fixme.rs
similarity index 100%
rename from tests/kani/BitwiseShiftOperators/shift_neg_vals.rs
rename to tests/kani/BitwiseShiftOperators/shift_neg_vals_fixme.rs
diff --git a/tests/kani/FatPointers/boxmuttrait.rs b/tests/kani/FatPointers/boxmuttrait_fixme.rs
similarity index 100%
rename from tests/kani/FatPointers/boxmuttrait.rs
rename to tests/kani/FatPointers/boxmuttrait_fixme.rs
diff --git a/tests/kani/FatPointers/boxslice1.rs b/tests/kani/FatPointers/boxslice1_fixme.rs
similarity index 100%
rename from tests/kani/FatPointers/boxslice1.rs
rename to tests/kani/FatPointers/boxslice1_fixme.rs
diff --git a/tests/kani/Intrinsics/PtrOffsetFrom/main.rs b/tests/kani/Intrinsics/PtrOffsetFrom/main_fixme.rs
similarity index 100%
rename from tests/kani/Intrinsics/PtrOffsetFrom/main.rs
rename to tests/kani/Intrinsics/PtrOffsetFrom/main_fixme.rs
diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift_fixme.rs
similarity index 100%
rename from tests/kani/Intrinsics/SIMD/Operators/bitshift.rs
rename to tests/kani/Intrinsics/SIMD/Operators/bitshift_fixme.rs
diff --git a/tests/kani/Iterator/flat_map.rs b/tests/kani/Iterator/flat_map_fixme.rs
similarity index 100%
rename from tests/kani/Iterator/flat_map.rs
rename to tests/kani/Iterator/flat_map_fixme.rs
diff --git a/tests/kani/PointerOffset/offset_from.rs b/tests/kani/PointerOffset/offset_from_fixme.rs
similarity index 100%
rename from tests/kani/PointerOffset/offset_from.rs
rename to tests/kani/PointerOffset/offset_from_fixme.rs
diff --git a/tests/kani/Refs/main.rs b/tests/kani/Refs/main_fixme.rs
similarity index 100%
rename from tests/kani/Refs/main.rs
rename to tests/kani/Refs/main_fixme.rs
diff --git a/tests/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/kani/Strings/copy_empty_string_by_intrinsic_fixme.rs
similarity index 100%
rename from tests/kani/Strings/copy_empty_string_by_intrinsic.rs
rename to tests/kani/Strings/copy_empty_string_by_intrinsic_fixme.rs
diff --git a/tests/kani/Vectors/any/push_slow.rs b/tests/kani/Vectors/any/push_slow_fixme.rs
similarity index 100%
rename from tests/kani/Vectors/any/push_slow.rs
rename to tests/kani/Vectors/any/push_slow_fixme.rs
diff --git a/tests/kani/Vectors/any/sorting.rs b/tests/kani/Vectors/any/sorting_fixme.rs
similarity index 100%
rename from tests/kani/Vectors/any/sorting.rs
rename to tests/kani/Vectors/any/sorting_fixme.rs
diff --git a/tests/ui/concrete-playback/unsupported/expected b/tests/ui/concrete-playback/unsupported/expected
index 67952ac37055..5d7424e34cf2 100644
--- a/tests/ui/concrete-playback/unsupported/expected
+++ b/tests/ui/concrete-playback/unsupported/expected
@@ -1,2 +1,2 @@
-Failed Checks: unwinding assertion loop 0
+Failed Checks: unwinding assertion loop 1
 WARNING: Kani could not produce a concrete playback for `check_unwind_fail` because there were no failing panic checks or satisfiable cover statements.
diff --git a/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs b/tests/ui/loop-contracts-synthesis/main_signed/main_signed_fixme.rs
similarity index 100%
rename from tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs
rename to tests/ui/loop-contracts-synthesis/main_signed/main_signed_fixme.rs
diff --git a/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned_fixme.rs
similarity index 100%
rename from tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
rename to tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned_fixme.rs
diff --git a/tests/ui/solver-attribute/cadical/test.rs b/tests/ui/solver-attribute/cadical/test.rs
index d8e897f923fb..2c4feaa4c356 100644
--- a/tests/ui/solver-attribute/cadical/test.rs
+++ b/tests/ui/solver-attribute/cadical/test.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `cadical` is a valid argument to `kani::solver`
 
diff --git a/tests/ui/solver-option/bin/test.rs b/tests/ui/solver-option/bin/test.rs
index 3529deb0eea9..c79618ecd028 100644
--- a/tests/ui/solver-option/bin/test.rs
+++ b/tests/ui/solver-option/bin/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver bin=kissat
+// kani-flags: --solver bin=kissat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `--solver` accepts `bin=<binary>`
 
diff --git a/tests/ui/solver-option/cadical/test.rs b/tests/ui/solver-option/cadical/test.rs
index a7b6e1304bf3..8742c1e2df87 100644
--- a/tests/ui/solver-option/cadical/test.rs
+++ b/tests/ui/solver-option/cadical/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver cadical
+// kani-flags: --solver cadical --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that the `cadical` is supported as an argument to `--solver`
 
diff --git a/tests/ui/solver-option/kissat/test.rs b/tests/ui/solver-option/kissat/test.rs
index 0b1403132ae3..4d876cdb952f 100644
--- a/tests/ui/solver-option/kissat/test.rs
+++ b/tests/ui/solver-option/kissat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver kissat
+// kani-flags: --solver kissat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that the solver option overrides the solver attribute
 
diff --git a/tests/ui/solver-option/minisat/test.rs b/tests/ui/solver-option/minisat/test.rs
index b92a4cd1b6c6..44778fd4f704 100644
--- a/tests/ui/solver-option/minisat/test.rs
+++ b/tests/ui/solver-option/minisat/test.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --solver minisat
+// kani-flags: --solver minisat --enable-unstable --cbmc-args --verbosity 9
 
 //! Checks that `--solver minisat` is accepted