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

author	Tim King <taking@google.com>
	Thu, 5 Nov 2015 22:18:03 +0000 (14:18 -0800)
committer	Tim King <taking@google.com>
	Thu, 5 Nov 2015 22:18:03 +0000 (14:18 -0800)
commit	859ae93590062ba7fef5577c6577068f0b74c239
tree	81d2d257c28414d10a261c242c1801f3eaadce78	tree
parent	b455f5cde8b84b7951d309604b75a76afd8b8bfa	commit \| diff

Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.

20 files changed:

src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_equality_engine.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
test/regress/regress0/bug605.cvc		diff \| blob \| history
test/regress/regress0/datatypes/cdt-model-cade15.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/floor.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/is-int.smt2		diff \| blob \| history
test/regress/regress0/strings/bug686dd.smt2		diff \| blob \| history
test/regress/regress0/strings/chapman150408.smt2		diff \| blob \| history
test/regress/regress0/strings/crash-1019.smt2		diff \| blob \| history
test/regress/regress0/strings/ilc-l-nt.smt2		diff \| blob \| history
test/regress/regress0/strings/ilc-like.smt2		diff \| blob \| history
test/regress/regress0/strings/indexof-sym-simp.smt2		diff \| blob \| history
test/regress/regress0/strings/kaluza-fl.smt2		diff \| blob \| history
test/regress/regress0/strings/norn-ab.smt2		diff \| blob \| history
test/regress/regress0/strings/norn-simp-rew.smt2		diff \| blob \| history
test/regress/regress0/strings/unsound-0908.smt2		diff \| blob \| history
test/regress/regress0/uf/cnf-and-neg.smt2		diff \| blob \| history
test/regress/regress0/uf/cnf_abc.smt2		diff \| blob \| history

RSS Atom