diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md index 2859d011a..6b0730dce 100644 --- a/quint/io-cli-tests.md +++ b/quint/io-cli-tests.md @@ -689,11 +689,11 @@ exit $exit_code ] ``` -### Test does not mean assignments (#1133) +### Test does not skip assignments (#1133) See: https://github.com/informalsystems/quint/issues/1133 -FIXME +FIXME: fix the traces found by the simulator once #1133 is resolved. ``` diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index 1cd410596..dbf5dac6e 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -260,7 +260,7 @@ export class CompilerVisitor implements IRVisitor { eval: () => { if (app.opcode === inputDefName) { this.execListener.onUserOperatorCall(evalApp) - // do not return from '_', as it may span over multiple frames + // do not call onUserOperatorReturn on '_' later, as it may span over multiple frames } else { this.execListener.onUserOperatorCall(app) } diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index b8d28b358..8ab821440 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -227,7 +227,9 @@ class TraceRecorderImpl implements TraceRecorder { if (verbosity.hasUserOpTracking(this.verbosityLevel)) { const newFrame = { app: app, args: [], result: none(), subframes: [] } if (this.frameStack.length == 0) { - // this should not happen, as there is always bottomFrame, but let's handle it + // this should not happen, as there is always bottomFrame, + // but we do not throw here, as trace collection is not the primary + // function of the simulator. this.frameStack = [newFrame] } else if (this.frameStack.length === 2 && this.frameStack[1].app.opcode === '_') { // A placeholder frame created from `q::input` or `then`. Modify in place.