diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs
index 68e094000884..77aa90ac4b00 100644
--- a/cprover_bindings/src/irep/irep.rs
+++ b/cprover_bindings/src/irep/irep.rs
@@ -47,8 +47,8 @@ impl Irep {
     /// Adds a `comment` sub to the irep.
     /// Note that there might be comments both on the irep itself and
     /// inside the location sub of the irep.
-    pub fn with_comment<T: Into<InternedString>>(self, c: T) -> Self {
-        self.with_named_sub(IrepId::Comment, Irep::just_string_id(c))
+    pub fn with_kani_comment<T: Into<InternedString>>(self, c: T) -> Self {
+        self.with_named_sub(IrepId::KaniComment, Irep::just_string_id(c))
     }
 
     pub fn with_named_sub(mut self, key: IrepId, value: Irep) -> Self {
diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs
index 3ad8f71a7e86..fee2a9bd538f 100644
--- a/cprover_bindings/src/irep/irep_id.rs
+++ b/cprover_bindings/src/irep/irep_id.rs
@@ -40,6 +40,7 @@ pub enum IrepId {
     Line,
     Column,
     Comment,
+    KaniComment,
     Property,
     PropertyClass,
     PropertyId,
@@ -909,6 +910,7 @@ impl ToString for IrepId {
             IrepId::Line => "line",
             IrepId::Column => "column",
             IrepId::Comment => "comment",
+            IrepId::KaniComment => "#kani_comment",
             IrepId::Property => "property",
             IrepId::PropertyClass => "property_class",
             IrepId::PropertyId => "property_id",
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 3ba02e3bd97f..e5a407376480 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -440,7 +440,7 @@ impl ToIrep for StmtBody {
                 // So we translate identically to `nondet` here, but add a comment noting we wish it were poison
                 // potentially for other backends to pick up and treat specially.
                 code_irep(IrepId::Assign, vec![place.to_irep(mm), place.typ().nondet().to_irep(mm)])
-                    .with_comment("deinit")
+                    .with_kani_comment("deinit")
             }
             StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
             StmtBody::For { init, cond, update, body } => code_irep(