diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 7d0edf6f50e5..4eb48f9b444b 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -183,6 +183,7 @@ impl KaniSession {
 
         if self.args.checks.unwinding_on() {
             args.push("--unwinding-assertions".into());
+            args.push("--no-self-loops-to-assumptions".into());
         }
 
         if self.args.extra_pointer_checks {
diff --git a/tests/expected/function-contract/diverging_loop.expected b/tests/expected/function-contract/diverging_loop.expected
new file mode 100644
index 000000000000..05c2856a7c31
--- /dev/null
+++ b/tests/expected/function-contract/diverging_loop.expected
@@ -0,0 +1,3 @@
+Failed Checks: unwinding assertion loop 0
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/function-contract/diverging_loop.rs b/tests/expected/function-contract/diverging_loop.rs
new file mode 100644
index 000000000000..7c8315a4be05
--- /dev/null
+++ b/tests/expected/function-contract/diverging_loop.rs
@@ -0,0 +1,11 @@
+#[kani::ensures(result == 1)]
+fn foo() -> i32 {
+    loop {};
+    2
+}
+
+#[kani::proof_for_contract(foo)]
+#[kani::unwind(1)]
+fn check_foo() {
+    let _ = foo();
+}