这是可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行的命令胜利者，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
victor - 尝试使用 SMT 求解器解除验证条件
概要
胜利者 [单元]
商品描述
这个 胜利者 命令是 ViCToR (录像带) 简化了它的使用。 胜利者
将 SPARK 验证条件转换为 SMTlib 并将其提供给 SMT 求解器。
SPARK 附带了一个这样的 SMT 求解器， 另类，但可以使用其他求解器
如 CV3.
victor 的预期用途是释放 Simplifier 留下的真正 VC，而不是
替换简化器。 另请注意，ViCToR 被认为是一个实验性的
目前的特点。
本手册页仅总结了 胜利者 命令行标志，请参阅完整
VictorWrapper 手册了解更多信息。
配置
这些选项并不完全遵循通常的 GNU 命令行语法，因为选项以
一个破折号而不是通常的两个。
-h, -救命
显示命令行帮助。
-t=SECONDS
在这么多秒后（默认为 5）超时 SMT 求解器使用 极限。 至
禁用超时指定 0。
-米=兆字节
使用
极限.
-v 忽略任何 siv 文件的存在并仅处理 vcg 文件。 默认情况下，给定
a 单元 例如 foo，victor 将首先尝试处理 foo.siv 然后回退
到 foo.vcg。
-普通 普通模式 - 抑制时间和版本。
-求解器=求解器
指定替代 SMT 求解器。 默认情况下，我们使用 alt-ergo。 可以是 alt-
ergo、cvc3、yices 或 z3。 alt-ergo 求解器随 SPARK 一起分发。 cvc3
求解器是 Debian 的一部分。 yices 和 z3 求解器是专有的。
使用 onworks.net 服务在线使用 victor
