Updates to CVC 1.0a

• May 15th, 2002 -- several bugs have been fixed since the last update. Also, support for arbitrary precision arithmetic has been added to CVC by Sergey Berezin and Vijay Ganesh. Falsifying contexts printed with "WHERE" go through a simplification step now; at least in SAT mode, they should be smaller than they were.
• April 17th, 2002 -- a minor bug introduced in yesterday's update was fixed.
• April 16th, 2002 -- a bug reported by a researcher at the Weizmann Institute was fixed. The bug was that querying a conjunction behaved differently than querying each conjunct separately.
• April 10th, 2002 -- a performance bug in the preprocessor having to due with how LET expressions are handled was fixed.
• April 9th, 2002 -- a bug reported by a researcher at the Weizmann Institute was fixed. The bug was a failure correctly to handle the case when the solver for arithmetic equations returned FALSE (solvers can do this when the equation they are given is unsolvable). Also, an insidious memory leak was fixed.
• April 2nd, 2002 -- a bug in the Chaff glue code was fixed that led to assert-fails saying "No controlling input found". Also, a problem in how the links in various links/ subdirectories of the source release were setup was fixed. The sources should be compilable under gcc 3.0.x now, as well as 2.95.3.
• March 21st, 2002 -- a rare incompleteness bug in the array decision procedure was fixed.
• March 13th, 2002 -- a piece of the congruence closure algorithm for Shostak theories was misimplemented. This has been corrected, fixing a bug.
• March 11th, 2002 -- several nasty performance bugs fixed. Also, Chaff now is used as the fast SAT solver (before, GRASP was being used). Sources can now be downloaded, too.
• Feb. 18th, 2002 -- dumb bug in run_flea.sh fixed.
• Jan. 30th, 2002 -- fixed a dumb bug in arithmetic. A dumb performance problem was also fixed. Falsifying contexts printed by WHERE are now simplified. A nagging bug in printing was also tracked down and fixed. Also a problem where the type checker was not robust was fixed.
• Nov. 27th, 2001 -- fixed a few bugs. LETs are now allowed in types. Major improvements have been made to flea, which should now be able to check proofs for runs of CVC lasting no more than a few seconds in at most a few minutes.