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  Simplifier. 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)