Ensure ITF is produced also on successful runs

Author: bugarela

quint/io-cli-tests.md

@@ -683,6 +683,25 @@ rm out-itf-example.itf.json
 ]
 ```
 
+### Run without violation outputs ITF
+
+<!-- !test in sucessful run itf -->
+```
+quint run --out-itf=out-itf-example.itf.json --max-steps=5 --seed=123  ../examples/solidity/Coin/coin.qnt
+cat out-itf-example.itf.json | jq '.states[0]."balances"."#map"[0]'
+rm out-itf-example.itf.json
+```
+
+<!-- !test out sucessful run itf -->
+```
+[
+  "alice",
+  {
+    "#bigint": "0"
+  }
+]
+```
+
 ### Test outputs ITF
 
 TODO: output states after fix: https://github.com/informalsystems/quint/issues/288

quint/src/cliCommands.ts

@@ -549,6 +549,16 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
 
   const elapsedMs = Date.now() - startMs
 
+  if (prev.args.outItf) {
+    const trace = toItf(result.vars, result.states)
+    if (trace.isRight()) {
+      const jsonObj = addItfHeader(prev.args.input, result.outcome.status, trace.value)
+      writeToJson(prev.args.outItf, jsonObj)
+    } else {
+      return cliErr(`ITF conversion failed: ${trace.value}`, { ...simulator, errors: [] })
+    }
+  }
+
   switch (result.outcome.status) {
     case 'error':
       return cliErr('Runtime error', {
@@ -585,16 +595,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
         }
       }
 
-      if (prev.args.outItf) {
-        const trace = toItf(result.vars, result.states)
-        if (trace.isRight()) {
-          const jsonObj = addItfHeader(prev.args.input, result.outcome.status, trace.value)
-          writeToJson(prev.args.outItf, jsonObj)
-        } else {
-          return cliErr(`ITF conversion failed: ${trace.value}`, { ...simulator, errors: [] })
-        }
-      }
-
       return cliErr('Invariant violated', {
         ...simulator,
         status: result.outcome.status,