Merge pull request #1553 from informalsystems/gabriela/fix-init-n-traces

Hotfix: Properly reset metadata variables

CHANGELOG.md

@@ -12,6 +12,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed a problem where traces other than the first one when `--n-traces` > 1
+  and `--mbt` is true had the incorrect `action_taken` and `nondet_picks` values
+  (#1553).
+
 ### Security
 
 ## v0.22.3 -- 2024-10-28

quint/io-cli-tests.md

@@ -894,14 +894,16 @@ rm out-itf-example.itf.json
 
 <!-- !test in run with n-traces itf -->
 ```
-quint run --out-itf=out-itf-example.itf.json --n-traces=3 --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
+quint run --out-itf=out-itf-example.itf.json --n-traces=3 --mbt --max-steps=5 --seed=123  ../examples/tutorials/coin.qnt
 cat out-itf-example0.itf.json | jq '.["#meta"].status'
+cat out-itf-example1.itf.json | jq '.states[0].action_taken'
 rm out-itf-example*.itf.json
 ```
 
 <!-- !test out run with n-traces itf -->
 ```
 "ok"
+"init"
 ```
 
 ### Run to generate multiple ITF traces with violation

quint/src/runtime/impl/VarStorage.ts

@@ -140,6 +140,12 @@ export class VarStorage {
   reset() {
     this.vars.forEach(reg => (reg.value = initialRegisterValue(reg.name)))
     this.nextVars.forEach(reg => (reg.value = initialRegisterValue(reg.name)))
+    if (this.storeMetadata) {
+      this.actionTaken = undefined
+      this.nondetPicks.forEach((_, key) => {
+        this.nondetPicks.set(key, undefined)
+      })
+    }
   }
 
   /**