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

Age	Commit message (Collapse)	Author
2014-09-26	Clarify some licensing-related things.	Morgan Deters

2014-09-18	cvc4terminate infinite loop fix	Kshitij Bansal

2014-09-17	Fix fix. There are no unsat cores in 1.4	Kshitij Bansal

2014-09-17	Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.	Kshitij Bansal

2014-08-28	fixing bug580 caused by bad bv inequality explanation	lianah

2014-08-22	Fix incorrectly-labeled test.	Morgan Deters

2014-08-22	Fix operator-printing issue in SMT2.	Morgan Deters

2014-08-22	Fix SMT1 parser :extrasorts/:extrapreds.	Morgan Deters

2014-08-19	Produce error for bad indexed function names in SMT-LIB, remove antlr warning.	Morgan Deters

2014-08-18	Revert a8e0ce67 and add test case (resolves bug #578).	Morgan Deters
	This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.
2014-08-05	fixed bug575 for bv models	lianah

2014-08-04	Some fixes to symmetry breaker (resolves bug 576).	Morgan Deters

2014-07-13	New versioning for development version.	Morgan Deters

2014-07-13	Cutting release 1.4.1.4	Morgan Deters

2014-07-12	Status for new bug testcase.	Morgan Deters

2014-07-12	Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵	Morgan Deters
	for the report.
2014-07-11	Spelling.	Morgan Deters

2014-07-11	fix for windows build	Kshitij Bansal

2014-07-10	Merge pull request #48 from kbansal/segfaultfix	Kshitij Bansal
	Segfaultfix
2014-07-10	Merge pull request #49 from kbansal/cvcparser	Kshitij Bansal
	Cvcparser
2014-07-10	rm warning	Kshitij Bansal

2014-07-10	membership cvc token changed to `IS_IN' to avoid conflict with IN used for let	Kshitij Bansal

2014-07-10	Merge remote-tracking branch 'origin/master' into segfaultfix	Kshitij Bansal

2014-07-10	friendlyparser: go back upto 2 words looking for match	Kshitij Bansal

2014-07-10	reorganize friendlyparser, behavior unchanged	Kshitij Bansal

2014-07-09	sets cvc parser	Kshitij Bansal

2014-07-09	sets cvc printer	Kshitij Bansal

2014-07-04	initialize variables	Kshitij Bansal

2014-07-03	change lemma generation behavior	Kshitij Bansal
	don't store lemmas in a pending queue, instead generate them right away doing with pending queue is tricky, needs rethinking to do it properly
2014-07-02	Fix cut-release script for new configure rules.	Morgan Deters

2014-07-02	Minor.	Morgan Deters

2014-07-01	Update portfolio_util.cpp	Kshitij Bansal

2014-07-01	Fix path in CASC J7 scripts, and distribute them with tarball.	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2014-07-01	reword NEWS	Morgan Deters

2014-07-01	Merge pull request #44 from mdeters/prio-queue-updates	Morgan Deters
	BinaryHeap unit test and some usability/build fixes for the data structu...
2014-07-01	chat about thread creation	Kshitij Bansal

2014-06-30	Merge pull request #45 from mdeters/turn-off-strings-exp	Morgan Deters
	Turn strings-exp off by default (for the release)
2014-06-30	Update NEWS	Kshitij Bansal

2014-06-30	Merge pull request #47 from kbansal/sets	Kshitij Bansal
	Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are: SMTLIB: emptyset, singleton, insert, union, intersection, setminus, member, subset API: EMPTYSET, SINGLETON, INSERT, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET (those marked with [*] have changed or been added, others are as earlier) In the set-logic string use FS to enable sets. A not-so-well-tested perl command for translating old benchmarks: perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '
2014-06-30	Use FS as the set-logic string for theory of sets	Kshitij Bansal

2014-06-29	sets: "insert" operator	Kshitij Bansal
	new™! support for (insert (X (Set X)) (Set X) :right-associative) from the finte sets theory prosoal. e.g., (insert 1 2 3 4 (singleton 5))
2014-06-28	Automatically make SMT options from command-line option names, warn when not ↵	Morgan Deters
	possible.
2014-06-28	Fix bug in datatypes options specification	Morgan Deters

2014-06-27	Another fix for 32-bit (amends commit b825605).	Morgan Deters

2014-06-27	Fix for bug543	Clark Barrett

2014-06-27	Updated run script for QF_ABV	Clark Barrett

2014-06-26	Merge pull request #46 from mdeters/bug573	Kshitij Bansal
	Potential fix for bug 573.
2014-06-26	Fix for 32-bit (esp. win32 failing build).	Morgan Deters

2014-06-26	Merge tag 'smtcomp2014-resubmission'	Morgan Deters
	Conflicts: src/main/portfolio.cpp