victor - attempts to discharge verification conditions using SMT solvers
The victor command is a wrapper around ViCToR
(vct) which simplifies its use. ViCToR
translates SPARK verification conditions into SMTlib and feeds
them to an SMT solver. SPARK ships with one such SMT solver,
alt-ergo, but it is possible to use others
solvers such as cvc3.
The intended use of victor is to discharge true VCs left over by
the Simplifier and not replace the Simplifier. Please also note
that ViCToR is considered to be an experimental feature at the
This manual page only summarises the victor
command-line flags, please refer to the full VictorWrapper
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
Shows command-line help.
Time-out the SMT solver after this many seconds (by default
5) using ulimit. To disable time-out
Limit the SMT solver to this many MiB of virtual memory (by
default no limit) using ulimit.
Ignore the presence of any siv files and
process vcg files only. By default, given
a UNIT such as foo, victor will
first attempt to process foo.siv and then fall back to
Plain mode --- supress timings and versions.
Specifies an alternative SMT solver. By default we use
alt-ergo. Can be one of alt-ergo, cvc3, yices or z3. The
alt-ergo solver is distributed with SPARK. The cvc3 solver
is part of Debian. The yices and z3 solvers are proprietary.
This manual page was written by Florian Schanda
<email@example.com> 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.