projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3845f11) | patch
Always produce assertions (#8041)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 Feb 2022 03:55:07 +0000 (21:55 -0600)
committerGitHub <noreply@github.com>
Tue, 8 Feb 2022 03:55:07 +0000 (03:55 +0000)
commit18cf7ab96a810c0c599de7bc005db1b8b2c2146a
tree067bc7bfab5ac4baf4265064221db43dcf1d2167tree
parent3845f112ff053c6485fd5c00c5b0c87522157ca9commit | diff
Always produce assertions (#8041)

There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option.
12 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/java/io/github/cvc5/api/Solver.java diff | blob | history
src/options/smt_options.toml diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/assertions.h diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history
test/unit/api/java/SolverTest.java diff | blob | history