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

author	Morgan Deters <mdeters@gmail.com>
	Wed, 11 Apr 2012 16:31:03 +0000 (16:31 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Wed, 11 Apr 2012 16:31:03 +0000 (16:31 +0000)
commit	d01d291be3213368985f28d0072905c4f033d5ff
tree	8524a2b6a00c012221ecca9266c3ab9fb11989ed	tree
parent	889853e225687dfef36b15ca1dccf74682e0fd66	commit \| diff

merge from arrays-clark branch

44 files changed:

configure.ac		diff \| blob \| history
src/parser/smt/Smt.g		diff \| blob \| history
src/parser/smt/smt.cpp		diff \| blob \| history
src/parser/smt/smt.h		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/array_info.h		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/bv/bitblast_strategies.cpp		diff \| blob \| history
src/theory/bv/bv_sat.cpp		diff \| blob \| history
src/theory/bv/bv_sat.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.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.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_impl.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/ntuple.h		diff \| blob \| history
test/Makefile.am		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/x2.smt	[new file with mode: 0644]	blob
test/regress/regress0/arrays/x3.smt	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/bug00.smt	[new file with mode: 0644]	blob

RSS Atom