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

Age	Commit message (Collapse)	Author
2014-07-01	Update copyrights.	Morgan Deters

2014-05-27	fix timespec printing	Kshitij Bansal
	sorry prvs fix added some unrelated code
2014-05-27	Revert "timespec printing bug"	Kshitij Bansal
	This reverts commit 9006b759cfa01c6006196e0716c2d67c760556a6.
2014-05-27	timespec printing bug	Kshitij Bansal

2014-03-04	Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵	Morgan Deters
	(resolves bug #548).
2014-02-20	portfolio: add stat to track time spent waiting for interrupted threads to stop	Kshitij Bansal

2013-12-10	Fix timer statistics to report correct time even on process abort.	Morgan Deters

2013-09-13	Documentation fixes, some code typo fixes, file perms, other minor things.	Morgan Deters

2013-04-26	FCSimplex branch merge	Tim King

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-01-31	Fix a small problem in clang builds due to namespaces and symbol lookup	Morgan Deters

2013-01-28	Fixes for Win32 (closes bugs 488 and 489)	Morgan Deters
	* timer statistics now supported (closes bug 488) * use of --mmap doesn't crash anymore (closes bug 489)
2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2013-01-25	Fix errors and reduce warnings on clang (merge from mdeters/clang)	Morgan Deters

2013-01-24	Add win32 support (merge from mdeters/win32, with some cleanup).	Morgan Deters

2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-28	fix production-build linking error	Morgan Deters

2012-09-28	Public interface review items:	Morgan Deters
	* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-09-24	Fix the memout issue seen in recent nightly regressions (was due to a	Morgan Deters
	Statistics-printing problem, limited to certain benchmarks). Mark some unlabeled header files "cvc4_private.h". Other minor cleanup. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-22	Separate public-facing and internal-facing interfaces to Statistics.	Morgan Deters
	The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry). The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it). This is part of the ongoing effort to clean up the public interface. (this commit was certified error- and warning-free by the test-and-commit script.)