summaryrefslogtreecommitdiff
path: root/src/expr/node_value.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-10-08 23:24:42 -0700
committerGitHub <noreply@github.com>2019-10-08 23:24:42 -0700
commit24f129a63b395a13ba10a05ff128e8e27ba75ed5 (patch)
tree143ed7f10733c5db326ae17ec51b680ce7a8f4fa /src/expr/node_value.h
parent1d4c28c9211db363b716b33954644d200b91dfd8 (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.
Diffstat (limited to 'src/expr/node_value.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback