NAME

       victor - attempts to discharge verification conditions using SMT solvers

SYNOPSIS

       victor [UNIT]

DESCRIPTION

       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 Sim‐
       plifier. Please also note that ViCToR is considered to be an experimental feature at the moment.

       This manual page only summarises the victor command-line flags, please refer to  the  full  VictorWrapper
       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.

       -h, -help
              Shows command-line help.

       -t=SECONDS
              Time-out the SMT solver after this many seconds (by default 5) using ulimit. To  disable  time-out
              specify 0.

       -m=MEGABYTES
              Limit the SMT solver to this many MiB of virtual memory (by default no limit) using ulimit.

       -v     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 foo.vcg.

       -plain Plain mode — supress timings and versions.

       -solver=SOLVER
              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.

SEE ALSO

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

       sparkformat(1), sparkmake(1)

       cvc3(1)

AUTHOR

       This  manual  page  was  written  by  Florian  Schanda <florian.schanda@altran-praxis.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.

                                                  22 March 2011                                        victor(1)