---
name: "spadesimp"
section: "1"
platform: "linux"
package: "spark"
version: "2012.0.deb-11+b2"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/spadesimp"
---

# spadesimp(1)

simplifies SPARK verification conditions

## NAME

spadesimp - simplifies SPARK verification conditions

## SYNOPSIS

**spadesimp**  \[OPTIONS\] \[UNIT\]

## DESCRIPTION

The Simplifier for SPARK, **spadesimp**, analyses verification conditions generated by the Examiner for SPARK and attempts to discharge them automatically. For each FCvcgF\[0\] file read, the Simplifier will produce a FCsivF\[0\] (simplified vcs) file and an optional FCslgF\[0\] (simplifier log) file.

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

## OPTIONS

These options do not quite follow the usual GNU command line syntax as options start with a single dash instead of the usual two.

- FC**-help**F\[0\]

  Displays command line help.

- FC**-version**F\[0\]

  Displays version information.

- FC**-nolog**F\[0\]

  Do not generate a simplification log file.

- FC**-log=**F\[0\]*file\_spec*

  Specify filename for the simplification log file.

- FC**-nowrap**F\[0\]

  Do not line wrap output files.

- FC**-verbose**F\[0\]

  Display attempted simplification strategies.

- FC**-nouserrules**F\[0\]

  Do not use user rules.

- FC**-plain**F\[0\]

  Adopt a plain output style (e.g. no dates or version numbers).

- FC**-typecheck**F\[0\]

  Only typecheck the input files.

- FC**-norenum**F\[0\]

  Do not renumber hypotheses and conclusions in FCsivF\[0\] files.

- FC**-nosimplification=**F\[0\]*RANGES*, FC**-nostandardisation=**F\[0\]*RANGES*, FC**-norule\_substitution=**F\[0\]*RANGES*, FC**-nocontradiction\_hunt=**F\[0\]*RANGES*, FC**-nosubstitution\_elimination=**F\[0\]*RANGES*, FC**-noexpression\_reduction=**F\[0\]*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.

- FC**-complexity\_limit=**F\[0\]*LIMIT*

  (Limit in range 10 .. 200)

- FC**-depth\_limit=**F\[0\]*LIMIT*

  (Limit in range 1 .. 10)

- FC**-inference\_limit=**F\[0\]*LIMIT*

  (Limit in range 10 .. 400)

## SEE ALSO

[spark(1)](/spark/1.md), [sparksimp(1)](/sparksimp/1.md), [zombiescope(1)](/zombiescope/1.md), [victor(1)](/victor/1.md), [pogs(1)](/pogs/1.md)

[sparkformat(1)](/sparkformat/1.md), [sparkmake(1)](/sparkmake/1.md)

## AUTHOR

This manual page was written by Florian Schanda \<FCflorian.schanda@altran-praxis.comF\[0\]\> 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.