Provided by: spark_2012.0.deb-11build1_amd64 bug


       spadesimp - 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.

       -help  Displays command line help.

              Displays version information.

       -nolog 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.

       -plain 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,
              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)


       spark(1), sparksimp(1), zombiescope(1), victor(1), pogs(1)

       sparkformat(1), sparkmake(1)


       This  manual  page  was written by Florian Schanda <> 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.

                                          22 March 2011                              spadesimp(1)