'\" -*- coding: us-ascii -*-
.if \n(.g .ds T< \\FC
.if \n(.g .ds T> \\F[\n[.fam]]
.de URL
\\$2 \(la\\$1\(ra\\$3
..
.if \n(.g .mso www.tmac
.TH victor 1 "22 March 2011" "" ""
.SH NAME
victor \- attempts to discharge verification conditions using SMT solvers 
.SH SYNOPSIS
'nh
.fi
.ad l
\fBvictor\fR \kx
.if (\nx>(\n(.l/2)) .nr x (\n(.l/5)
'in \n(.iu+\nxu
[UNIT]
'in \n(.iu-\nxu
.ad b
'hy
.SH DESCRIPTION
The \fBvictor\fR command is a wrapper around ViCToR
(\fBvct\fR) 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,
\fBalt-ergo\fR, but it is possible to use others
solvers such as \fBcvc3\fR.
.PP
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.
.PP
This manual page only summarises the \fBvictor\fR
command-line flags, please refer to the full VictorWrapper
manual for further information.
.SH 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.
.TP 
\*(T<\fB\-h\fR\*(T>, \*(T<\fB\-help\fR\*(T>
Shows command-line help.
.TP 
\*(T<\fB\-t=\fR\*(T>\fISECONDS\fR
Time-out the SMT solver after this many seconds (by default
5) using \fBulimit\fR. To disable time-out
specify 0.
.TP 
\*(T<\fB\-m=\fR\*(T>\fIMEGABYTES\fR
Limit the SMT solver to this many MiB of virtual memory (by
default no limit) using \fBulimit\fR.
.TP 
\*(T<\fB\-v\fR\*(T>
Ignore the presence of any \*(T<siv\*(T> files and
process \*(T<vcg\*(T> files only. By default, given
a \fIUNIT\fR such as foo, victor will
first attempt to process foo.siv and then fall back to
foo.vcg.
.TP 
\*(T<\fB\-plain\fR\*(T>
Plain mode \[em] supress timings and versions.
.TP 
\*(T<\fB\-solver=\fR\*(T>\fISOLVER\fR
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.
.SH "SEE ALSO"
spark(1),
sparksimp(1),
spadesimp(1),
zombiescope(1),
pogs(1)
.PP
sparkformat(1), sparkmake(1)
.PP
cvc3(1)
.SH AUTHOR
This manual page was written by Florian Schanda
<\*(T<florian.schanda@altran\-praxis.com\*(T>> for the
\fIDebian GNU/Linux\fR 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.