projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a04226e) | patch
Dumping unsat cores after check-sat-assuming/QUERY (#5724)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 23 Dec 2020 23:10:34 +0000 (20:10 -0300)
committerGitHub <noreply@github.com>
Wed, 23 Dec 2020 23:10:34 +0000 (17:10 -0600)
commita539b63c369544ed08a1fa7fa4c8e3d437be3766
tree033ba2288164e43c8d91c772fd63d0905d74a6e8tree
parenta04226ef3519c4fdce7bd6c3ff92f18bf6bee83ccommit | diff
Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.
src/main/command_executor.cpp diff | blob | history
src/options/options.h diff | blob | history
src/options/options_public_functions.cpp diff | blob | history
src/options/smt_options.toml diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history