Error when running `quint test --verbosity=x` where x in {3,4,5}

[p-offtermatt]

My spec is here: https://github.com/cosmos/interchain-security/blob/c69977414782ed604f53cf555e342bb177163123/tests/mbt/model/ccv_model.qnt#L523

When I run

quint test ccv_model.qnt --verbosity=3

I get this error:

TypeError: Cannot read properties of undefined (reading 'subframes')
    at TraceRecorderImpl.onNextState (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/trace.js:147:32)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1116:35)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1091:29)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)
    at CompilerVisitor.chainAllOrThen (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1091:29)
    at lazyCompute (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1129:40)
    at Object.eval (/opt/homebrew/lib/node_modules/@informalsystems/quint/dist/src/runtime/impl/compilerImpl.js:1541:20)

The same happens for verbosity 4 and 5. Everything works fine for lower verbosities.

It doesn't seem to be a general problem with verbosity in tests - I tried --verbosity=3 with this very simple module, and there everything works fine, so I assume it's something specific to my spec.

module a {
    var a: int

    action init: bool = a' = 1

    action foo: bool = a' = 2

    run FooTest = init.then(foo).then(all{a == 1, foo})
}

$ quint test test.qnt --verbosity=3

  a
    1) FooTest failed after 1 test(s)

  1 failed

  1) FooTest:
      /Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:8:5 - error: [QNT511] Test FooTest returned false
      8:     run FooTest = init.then(foo).then(all{a == 1, foo})

[Frame 0]
init => true

[Frame 1]
foo => true

[Frame 2]
_ => none

    Use --seed=0x327e8c85f463b --match=FooTest to repeat.

/Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:8:5 - error: [QNT511] Test FooTest returned false
8:     run FooTest = init.then(foo).then(all{a == 1, foo})
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Tests failed