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