spadesimp(1) simplifies SPARK verification conditions


spadesimp [OPTIONS] [UNIT]


The Simplifier for SPARK, spadesimp, analyses verification conditions generated by the Examiner for SPARK and attempts to discharge them automatically. For each vcg file read, the Simplifier will produce a siv (simplified vcs) file and an optional slg (simplifier log) file.

This manual page only summarises the spadesimp command-line flags, please refer to the full Simplifier manual for further information.


These options do not quite follow the usual GNU command line syntax as options start with a single dash instead of the usual two.
Displays command line help.
Displays version information.
Do not generate a simplification log file.
Specify filename for the simplification log file.
Do not line wrap output files.
Display attempted simplification strategies.
Do not use user rules.
Adopt a plain output style (e.g. no dates or version numbers).
Only typecheck the input files.
Do not renumber hypotheses and conclusions in siv files.
-nosimplification=RANGES, -nostandardisation=RANGES, -norule_substitution=RANGES, -nocontradiction_hunt=RANGES, -nosubstitution_elimination=RANGES, -noexpression_reduction=RANGES
Adjust strategy for different VCs. RANGES can be a comma separated list of ranges. Each range can be either a single VC number or a simple range of the form VC-VC.
(Limit in range 10 .. 200)
(Limit in range 1 .. 10)
(Limit in range 10 .. 400)


This manual page was written by Florian Schanda <[email protected]> for the Debian GNU/Linux system (but may be used by others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-Cover Texts.