projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1d4c28c) | patch
Avoid printing success for `--force-logic` (#3363)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 9 Oct 2019 06:24:42 +0000 (23:24 -0700)
committerGitHub <noreply@github.com>
Wed, 9 Oct 2019 06:24:42 +0000 (23:24 -0700)
commit24f129a63b395a13ba10a05ff128e8e27ba75ed5
tree143ed7f10733c5db326ae17ec51b680ce7a8f4fatree
parent1d4c28c9211db363b716b33954644d200b91dfd8commit | diff
Avoid printing success for `--force-logic` (#3363)

CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.

The issue was likely introduced with #3062.
src/parser/smt2/smt2.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/force_logic_success.smt2 [new file with mode: 0644] blob