print the seed on success (#1213)

* print the seed on success * update the changelog * Update CHANGELOG.md Co-authored-by: Thomas Pani <[email protected]> --------- Co-authored-by: Thomas Pani <[email protected]>
informalsystems · Oct 11, 2023 · e01043c · e01043c
1 parent b00b835
commit e01043c
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 
 - Error messages for `val` vs `def` and `pure val` vs `pure def` errors are clearer (#1208)
+- `quint run` prints the random seed even if no bug was found (#1213)
 
 ### Deprecated
 ### Removed

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
@@ -421,6 +421,7 @@ An example execution:
 [State 4] { n: 12 }
 
 [ok] No violation found (duration).
+Use --seed=0x11 to reproduce.
 You may increase --max-samples and --max-steps.
 Use --verbosity to produce more (or less) output.
 ```

diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
@@ -519,6 +519,7 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       maybePrintCounterExample(verbosityLevel, result.states, result.frames)
       if (result.status === 'ok') {
         console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
+        console.log(chalk.gray(`Use --seed=0x${result.seed.toString(16)} to reproduce.`))
         if (verbosity.hasHints(options.verbosity)) {
           console.log(chalk.gray('You may increase --max-samples and --max-steps.'))
           console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))