v5.1.1 (August 2025 release)

Release 2025.8

Date 04/09/25

Viper-IDE & ViperServer

• Significantly enhanced IDE experience (viperproject/viperserver#204 and #433 and others):
  • Enabled semantic code actions such as "Show / Jump to Definitions", "Find References" or "Rename Symbols"
  • Improved autocomplete
  • Show inferred triggers
  • Show parameter names in method calls
  • Show parser errors without triggering full verification
• Reworked extension settings. Some custom settings have been renamed and may need to be updated.

Changes in Viper Language

• The annotation previously called @proverArgs, (i.e. for example @proverArgs("smt.arith.solver=6")) is now called @proverConfigArgs to match the name of Silicon's corresponding command line option --proverConfigArgs. viperproject/silicon#932
• asserting-expressions are now disallowed in domain axioms. viperproject/silver#858
• We changed the type priority of ambiguously-typed division expressions (e.g. 1/2 can be an Int or a Perm); these now always default to be Perm-typed, and an Int type can be enforced by using the \ operator instead. viperproject/silver#855

Changes in Plugins

• Plugins can now specify whether new expression types added by the plugin can be used inside triggers. viperproject/silver#857
• Created a new PluginAwareReporter that allows plugins to transform EntitySuccessMessages and EntityFailureMessages. viperproject/silver#854 and viperproject/silver#856
• Optimized encoding for termination checks to omit unnecessary expression evaluation and unfoldings. viperproject/silver#879
• Fixed incomplete termination check encoding for functions which incorrectly used explicit permission amounts. viperproject/silver#876

Other Changes and Bug Fixes

• Fixed a crash in the type checker for some forperm expressions. viperproject/silver#873
• Removed unnecessary duplicate work in the type checker that could lead to non-termination in extreme cases. viperproject/silver#865
• Fixed loop head detection that could in rare cases lead to unsound verification. viperproject/silver#859
• Improved Simplifier to simplify more aggressively in the presence of expressions that are statically known to be well-defined. viperproject/silver#863
• No longer using sets internally so that the plugin execution order is always deterministic. viperproject/silver#853

Backend-specific Upgrades/Changes

Symbolic Execution Backend (Silicon)

• A new command line option --enableSimplifiedUnfolds can be used to simplify and speed up predicate unfoldings. It is experimental and disabled by default for now, but will likely become the default setting in future releases. viperproject/silicon#929
• Soundness fixes:
  • Fixed two unsoundnesses in heap-dependent function encoding resulting from state consolidation. viperproject/silicon#904 and viperproject/silicon#910
  • Fixed incorrect translation of some heap accesses inside heap-dependent functions that could lead to crashes or the use of incorrect function definitions. viperproject/silicon#928
• Performance improvements:
  • Localizing potentially expensive assumption of function preconditions for QP injectivity. viperproject/silicon#916
  • Simplifying checks about permission amounts inside functions s.t. they can more often be performed without use of the SMT solver. viperproject/silicon#921
  • Stricter triggers on expensive extensionality axiom for QP snapshots (used for framing functions that depend on QPs). viperproject/silicon#936
• Completeness fixes:
  • Fixing incorrect usage of (shorter) check timeout for SMT query that should use the assert timeout, leading to incompleteness. viperproject/silicon#920
  • Fixed recording of QP-related definitions in heap-dependent functions that was previously missing. viperproject/silicon#924
  • Fixed an incompleteness where QP-related definitions generated while evaluating quantifiers used an arbitrary value of the quantified variable instead of a universally quantified one viperproject/silicon#93
• Bug fixes:
  • Fixed --counterexample=variables option. viperproject/silicon#915
  • Fixed crash with --moreJoins option when using forperm. viperproject/silicon#922
  • Fixed crash with branch parallelization. viperproject/silicon#939
• Others:
  • When using CVC5, Silicon is now using proper timeouts for its SMT queries. viperproject/silicon#933
  • Quantifiers in axioms related to built-in types like sequences now have quantifier IDs in the generated SMTLIB code, which simplifies debugging the SMT output. viperproject/silicon#927
  • Significant parts of Silicon have been refactored to simplify future extensions, in particular, to enable the addition of different heap encodings. viperproject/silicon#930

Based on

• ViperServer release v.25.08-release
• Z3 4.8.7
• Boogie release 7449a7a899c02c95