[Bug 529404] Review Request: cvc3 - Validity checker of many-sorted first-order formulas with theories

[bugzilla at redhat.com]

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


https://bugzilla.redhat.com/show_bug.cgi?id=529404





--- Comment #4 from Jerry James <loganjerry at gmail.com>  2009-10-19 17:02:35 EDT ---
New URLs:

http://jjames.fedorapeople.org/cvc3/cvc3.spec
http://jjames.fedorapeople.org/cvc3/cvc3-2.1-2.fc11.src.rpm

I have made the following changes:
- The Java code is now built (it required a little patching to get the JNI code
to build).
- The %makeinstall macro is now used.
- The empty PNG is a result of dot segfaulting on some really big input.  For
now, I'm letting it segfault and just removing the empty file.  Long term, I'll
try to get dot to generate good input, or make doxygen stop asking dot to
process that file.
- The unstripped library was due to the .so file not having the executable bits
turned on.  This is now fixed.
- The files with missing " symbols are patched, so doxygen no longer complains.
- The API documentation is now in a separate -doc package.

I am not going to touch the useless rule warnings generated by bison, as I'm
not certain I can do so without damaging the grammar files.  We should report
this upstream and see if they can fix it, though.

I initially added the %check section that you suggested.  However, when I
enabled Java support, %check stopped working because it couldn't find the JAR
files.  There's probably an easy fix for that, but I haven't had time to pursue
it yet.

The minisat code does appear to be related somehow to that in the minisat2
package, but it differs signficantly.  The minisat2 package supplies only a
binary, not a library, so I couldn't link with it in any case.  Even if it did
supply a library, I am uncertain of the significance of the differences between
the two code bases.  How do you suggest I proceed on this point?

-- 
Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.