Merge pull request #3010 from apalache-mc/igor/vcgen-source

add source tracking in VCGenerator
apalache-mc · Oct 8, 2024 · 270175c · 270175c
2 parents 9e9d099 + 938b5c8
commit 270175c
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/.unreleased/bug-fixes/source-tracking-in-vcgen.md 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
@@ -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)
     }
   }
 }