cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2010-03-08	This fixes regressions at levels >= 1 which were failing	Morgan Deters
	* implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting
2010-02-04	build system for multi-level regressions	Morgan Deters

2010-02-04	test infrastructure updated for multiple-level regressions	Morgan Deters

2010-01-27	support "make check" in src/ subdirs for unit-testing of just that module; ↵	Morgan Deters
	also support synonyms for "make check" globally
2010-01-27	test framework fixes; bug 13 closed	Morgan Deters

2009-12-17	add system regression testing infrastructure	Morgan Deters