Merge pull request #1491 from informalsystems/romac/fix-verify-itf-fo…

…rmat Fix format of ITF trace emitted by `verify` command
informalsystems · Sep 2, 2024 · 351b52a · 351b52a
2 parents 396e4c1 + 44a66d2
commit 351b52a
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -29,7 +29,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Fixed
 
- - Bumped GRPC message sizes to 1G (#1480)
+- Bumped GRPC message sizes to 1G (#1480)
+- Fix format of ITF trace emitted by `verify` command (#1448)
 
 ### Security
 

diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md
@@ -119,7 +119,7 @@ An example execution:
 <!-- !test in writes an ITF trace to file -->
 ```
 quint verify --out-itf violateOnFive.itf.json --invariant inv ./testFixture/apalache/violateOnFive.qnt
-jq '.[0]."#meta".format' violateOnFive.itf.json
+jq '."#meta".format' violateOnFive.itf.json
 rm ./violateOnFive.itf.json
 ```
 

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
@@ -805,8 +805,8 @@ export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<Trac
             console.log(chalk.red(`[${status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
           }
 
-          if (prev.args.outItf) {
-            writeToJson(prev.args.outItf, err.traces)
+          if (prev.args.outItf && err.traces) {
+            writeToJson(prev.args.outItf, err.traces[0])
           }
         }
         return {