diff --git a/src/cargo-kani/src/args.rs b/src/cargo-kani/src/args.rs
index 10b2b575d188..61d3eacfb250 100644
--- a/src/cargo-kani/src/args.rs
+++ b/src/cargo-kani/src/args.rs
@@ -75,8 +75,9 @@ pub struct KaniArgs {
     /// Entry point for verification
     #[structopt(long, default_value = "main")]
     pub function: String,
-    /// Link external C files referenced by Rust code
-    #[structopt(long, parse(from_os_str))]
+    /// Link external C files referenced by Rust code.
+    /// This is an experimental feature.
+    #[structopt(long, parse(from_os_str), hidden = true)]
     pub c_lib: Vec<PathBuf>,
     /// Enable test function verification. Only use this option when the entry point is a test function.
     #[structopt(long)]
diff --git a/src/cargo-kani/src/call_goto_instrument.rs b/src/cargo-kani/src/call_goto_instrument.rs
index 23c1c9481fc7..8e0d5fc46219 100644
--- a/src/cargo-kani/src/call_goto_instrument.rs
+++ b/src/cargo-kani/src/call_goto_instrument.rs
@@ -79,7 +79,7 @@ impl KaniSession {
     fn undefined_functions(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--generate-function-body-options".into(),
-            "assert-false".into(),
+            "assert-false-assume-false".into(),
             "--generate-function-body".into(),
             ".*".into(),
             "--drop-unused-functions".into(),
diff --git a/tests/ui/cbmc_checks/float-overflow/check_message.rs b/tests/ui/cbmc_checks/float-overflow/check_message.rs
index 24ece7e1d482..944404c3720a 100644
--- a/tests/ui/cbmc_checks/float-overflow/check_message.rs
+++ b/tests/ui/cbmc_checks/float-overflow/check_message.rs
@@ -8,7 +8,7 @@ use kani::any;
 
 // Use the result so rustc doesn't optimize them away.
 fn dummy(result: f32) -> f32 {
-    result.round()
+    result
 }
 
 #[kani::proof]
diff --git a/tests/ui/missing-function/expected b/tests/ui/missing-function/expected
new file mode 100644
index 000000000000..96d77b5fad4c
--- /dev/null
+++ b/tests/ui/missing-function/expected
@@ -0,0 +1,5 @@
+Status: UNREACHABLE\
+Description: "assertion failed: x == 5"
+
+VERIFICATION:- FAILED
+
diff --git a/tests/ui/missing-function/extern_c.rs b/tests/ui/missing-function/extern_c.rs
new file mode 100644
index 000000000000..b1d95f523f5b
--- /dev/null
+++ b/tests/ui/missing-function/extern_c.rs
@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --function harness
+
+// This test is to check Kani's error handling for missing functions.
+// TODO: Verify that this prints a compiler warning:
+//  - https://github.com/model-checking/kani/issues/576
+
+
+extern "C" {
+    fn missing_function() -> u32;
+}
+
+#[kani::proof]
+fn harness() {
+    let x = unsafe { missing_function() };
+    assert!(x == 5);
+}