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

author	Clark Barrett <barrett@cs.nyu.edu>
	Thu, 15 Nov 2012 21:27:33 +0000 (21:27 +0000)
committer	Clark Barrett <barrett@cs.nyu.edu>
	Thu, 15 Nov 2012 21:27:33 +0000 (21:27 +0000)
commit	a8ae064eb9ee7175e83eee29d03459b22aa158ef
tree	e2b432a9a1c4f835070b4c4c75a9912e138b54ac	tree
parent	88ef1f0be6bd712cf1ce8401416d634f61f381b4	commit \| diff

More fixes to model generation, with previously failing testcases
Also refactored some header file includes to reduce compile time

14 files changed:

src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/bv/bv_subtheory_eq.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/model.h		diff \| blob \| history
src/theory/rewriterules/theory_rewriterules.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
test/regress/regress0/auflia/Makefile.am		diff \| blob \| history
test/regress/regress0/auflia/fuzz05.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflra/Makefile.am		diff \| blob \| history
test/regress/regress0/uflra/fuzz01.smt	[new file with mode: 0644]	blob