Skip to content

Commit

Permalink
Merge pull request #727 from viperproject/meilers_releasenotes_237_fix
Browse files Browse the repository at this point in the history
Fixing a typo Gaurav found
  • Loading branch information
marcoeilers authored Aug 3, 2023
2 parents 87f83ec + c4b4891 commit 9f5b214
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ReleaseNotes.md
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@
- Silicon now emits warnings in cases where it cannot use the triggers specified by the user ([Silicon#687](https://github.com/viperproject/silicon/pull/687))
- ``old``-expressions in triggers are now interpreted correctly ([Silicon#710](https://github.com/viperproject/silicon/pull/710)); previously, they were sometimes ignored.
- Changed default options used for Z3; the new options have similar performance and completeness characteristics with the supported Z3 version 4.8.7, but perform better with newer versions (tested in particular with 4.12.1) ([Silicon#694](https://github.com/viperproject/silicon/pull/694))
- Silicon now longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``.
- Silicon no longer creates a ``tmp`` directory containing ``.smt2`` files that log its prover interactions by default ([Silicon#709](https://github.com/viperproject/silicon/pull/709)). The flag ``--disableTempDirectory`` no longer exists. Instead, one can use the new flag ``--enableTempDirectory`` or the flag ``--proverLogFile``.
- Improved heuristics for handling of quantified permissions, which improves performance in some cases ([Silicon#704](https://github.com/viperproject/silicon/pull/704))
- Fixed some incorrect (too short) timeouts, which could lead to unstable verification results in some cases ([Silicon#705](https://github.com/viperproject/silicon/pull/705))
- Added a new command line flag ``--reportReasonUnknown``, which instructs Silicon to report the reason the SMT solver names for not being able to prove a property (per error) ([Silicon#701](https://github.com/viperproject/silicon/pull/701)). This flag can be useful to find out whether an error occurred due to non-linear arithmetic or timeouts.
Expand Down

0 comments on commit 9f5b214

Please sign in to comment.