diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 6e896ee97288..50ece13fe193 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1730,7 +1730,7 @@ impl GotocCtx<'_> {
 
         // Check that computing `count` in bytes would not overflow
         let (count_bytes, overflow_check) = self.count_in_bytes(
-            count,
+            count.clone(),
             pointee_type_stable(dst_typ).unwrap(),
             Type::size_t(),
             "write_bytes",
@@ -1738,7 +1738,12 @@ impl GotocCtx<'_> {
         );
 
         let memset_call = BuiltinFn::Memset.call(vec![dst, val, count_bytes], loc);
-        Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
+        Stmt::if_then_else(
+            count.clone().gt(Expr::int_constant(0, count.typ().clone())),
+            Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc),
+            None,
+            loc,
+        )
     }
 
     /// Computes (multiplies) the equivalent of a memory-related number (e.g., an offset) in bytes.
diff --git a/tests/kani/NondetVectors/fixme_main.rs b/tests/kani/NondetVectors/main.rs
similarity index 62%
rename from tests/kani/NondetVectors/fixme_main.rs
rename to tests/kani/NondetVectors/main.rs
index 2b361b7b1bf1..84c7234b0410 100644
--- a/tests/kani/NondetVectors/fixme_main.rs
+++ b/tests/kani/NondetVectors/main.rs
@@ -16,3 +16,20 @@ fn main() {
         assert!(_buf2[idx] == elt);
     }
 }
+
+#[kani::proof]
+fn minimal1() {
+    let v: Vec<i8> = vec![kani::any(); 0];
+}
+
+#[kani::proof]
+fn minimal2() {
+    let v: Vec<i8> = vec![5; 0];
+}
+
+#[kani::proof]
+fn vec3772() {
+    let value: u8 = 1; /* set to zero and it passes */
+    let count: u16 = kani::any();
+    let vector: Vec<u8> = vec![value; count as usize];
+}