git.libre-soc.org Git - cvc5.git/commit

author	ajreynol <andrew.j.reynolds@gmail.com>
	Tue, 12 Apr 2016 21:29:20 +0000 (16:29 -0500)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Tue, 12 Apr 2016 21:29:20 +0000 (16:29 -0500)
commit	dd01099518aab8d42d788dfadadbe11763ec9d18
tree	ab3accd00c5e4ee3f2035349b9387bf8b9d85e90	tree
parent	4ff2946e1338d3f500b7e6bababee50fadad68d6	commit \| diff

Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.

src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
test/regress/regress0/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/parametric-lists.smt2	[new file with mode: 0644]	blob