1Ivy is a system that checks Otter proofs and MACE models.
2Ivy is coded in ACL2 and many soundness metatheorems have
3been proved about the various programs in Ivy.  See
4
5       http://www.mcs.anl.gov/~mccune/acl2/ivy
6
7Ivy-2 is the current version.  Otter-3.0.6 and MACE-1.3.4
8come bundled with Ivy-2.  If you wish to have Ivy-2 call Otter-3.3
9and MACE-2. instead, you can do so by updating 2 Ivy files (after
10configuring Ivy):
11
12ivy-v2/ivy-sources/util/otter-mace.lisp
13
14    Change the line
15        (defvar mace-parms "6 60 -m1 -I -c")
16    to
17        (defvar mace-parms "-N6 -t60 -I")
18
19ivy-v2/ivy-sources/util/ivy
20
21    Change the lines that begin
22
23        set otter_binary=
24        set mace_binary=
25
26    so that they refer to the Otter-3.3 and MACE-2.1 binaries, for example,
27
28        set otter_binary=/homes/mccune/bin-linux/otter33
29        set mace_binary=/homes/mccune/bin-linux/mace21
30