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.