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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Tue, 8 Nov 2016 16:09:53 +0000 (10:09 -0600)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Tue, 8 Nov 2016 16:10:08 +0000 (10:10 -0600)
commit	2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa
tree	960adfe7c475b1d5c54dbb4c43b035ee6c740151	tree
parent	1f9f7a3bd665575fd25f0fe93547ee0564cc18c9	commit \| diff

Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.

23 files changed:

src/options/sep_options		diff \| blob \| history
src/options/sets_options		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/model_engine.cpp		diff \| blob \| history
src/theory/sep/kinds		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
test/regress/regress0/sep/dispose-1.smt2		diff \| blob \| history
test/regress/regress0/sep/dup-nemp.smt2		diff \| blob \| history
test/regress/regress0/sep/emp2-quant-unsat.smt2		diff \| blob \| history
test/regress/regress0/sep/finite-witness-sat.smt2		diff \| blob \| history
test/regress/regress0/sep/fmf-nemp-2.smt2		diff \| blob \| history
test/regress/regress0/sep/nemp.smt2		diff \| blob \| history
test/regress/regress0/sep/quant_wand.smt2		diff \| blob \| history
test/regress/regress0/sep/sep-simp-unsat-emp.smt2		diff \| blob \| history
test/regress/regress0/sep/trees-1.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-0526-sat.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-crash.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-nterm-simp.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-nterm-simp2.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-simp-unsat.smt2		diff \| blob \| history