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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 27 May 2021 06:44:55 +0000 (01:44 -0500)
committer	GitHub <noreply@github.com>
	Thu, 27 May 2021 06:44:55 +0000 (06:44 +0000)
commit	437405dca0e1a393a8fa1eda900bc0bc469091c6
tree	4855b19b650818337aaad35ef9c4178e3645c5c0	tree
parent	028d657dc41bbb908b7b9ad6ba707dc2216b15ac	commit \| diff

Enable new justification heuristic by default (#6613)

This enables the new implementation of justification heuristic by default.

Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.

29 files changed:

contrib/competitions/smt-comp/run-script-smtcomp-current		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/justification_strategy.cpp		diff \| blob \| history
src/decision/justification_strategy.h		diff \| blob \| history
src/options/decision_options.toml		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/arith/div.05.smt2		diff \| blob \| history
test/regress/regress0/fp/issue3619.smt2		diff \| blob \| history
test/regress/regress0/fp/issue4277-assign-func.smt2		diff \| blob \| history
test/regress/regress0/issue5099-model-2.smt2		diff \| blob \| history
test/regress/regress1/decision/issue5454-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/issue5454-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/issue5454.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/issue5785.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/jh-test1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue114.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue115.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue116.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue149-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue149-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/wishue160.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/issue4420-order-sensitive.smt2		diff \| blob \| history
test/regress/regress2/strings/issue6483.smt2		diff \| blob \| history
test/regress/regress3/ho/SYO362^5.p		diff \| blob \| history

RSS Atom