bug in ladr_to_tptp on Macs

Transforming and Filtering Data

bug in ladr_to_tptp on Macs

Postby mccune on Mon Feb 22, 2010 6:29 pm

There is a bug in ladr_to_tptp (the utility that translates Prover9/Mace4 inputs to TPTP syntax) that seems to appear only on Macs. The bug causes
ladr_to_tptp to crash immediately. It is fixed for the next release.

If you need ladr_to_tptp before then, you can make the following change and recompile.

In file provers.src/ladr_to_tptp.c, find the line
Code: Select all
input = std_prover_init_and_input(0, NULL,

and change it to
Code: Select all
input = std_prover_init_and_input(1, argv,  // ignore command-line args

then recompile.

If your ladr_to_tptp does not crash, there's no need to make the change.

Bill
mccune
Site Admin
 
Posts: 84
Joined: Fri Apr 11, 2008 4:05 pm
Location: Placitas, New Mexico

Return to Other LADR Programs

Who is online

Users browsing this forum: No registered users and 1 guest

cron