diff --git a/.unreleased/bug-fixes/source-tracking-in-vcgen.md b/.unreleased/bug-fixes/source-tracking-in-vcgen.md
new file mode 100644
index 0000000000..04e361c2de
--- /dev/null
+++ b/.unreleased/bug-fixes/source-tracking-in-vcgen.md
@@ -0,0 +1 @@
+Fix source tracking in `VCGenerator` to avoid spurious diagnostic messages, see #3010
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala
index 62945021c0..22ebc0c79f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/VCGenerator.scala
@@ -67,6 +67,9 @@ class VCGenerator(tracker: TransformationTracker) extends LazyLogging {
           val notBody = tla.not(tla.fromTlaEx(copy.deepCopyEx(body))).typed(BoolT1)
           val negative =
             TlaOperDecl(NormalizedNames.VC_NOT_TRACE_INV_PREFIX + "0", params, notBody)(traceInv.typeTag)
+          // track the changes
+          tracker.hold(body, positive.body)
+          tracker.hold(body, negative.body)
           TlaModule(module.name, module.declarations :+ positive :+ negative)
 
         case Some(decl: TlaOperDecl) =>
@@ -166,7 +169,10 @@ class VCGenerator(tracker: TransformationTracker) extends LazyLogging {
         expr
 
       case (nameEx, set) :: tail =>
-        decorateWithUniversals(tail, tla.forall(nameEx, set, expr).typed(BoolT1))
+        val withForall = tla.forall(nameEx, set, expr).typed(BoolT1)
+        // remember the source of the change
+        tracker.hold(expr, withForall)
+        decorateWithUniversals(tail, withForall)
     }
   }
 }