projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 87cd311) | patch
Mute `define-fun` command generated for named terms. (#7788)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Fri, 10 Dec 2021 18:44:10 +0000 (12:44 -0600)
committerGitHub <noreply@github.com>
Fri, 10 Dec 2021 18:44:10 +0000 (18:44 +0000)
commit051a568564958be1433ff64a98808398c1f6e238
treea253c1539f497aafe32cba681a10e5c273f12260tree
parent87cd3112098d24b35cedabffdc5f927998a4e4b0commit | diff
Mute `define-fun` command generated for named terms. (#7788)

Kind 2 uses print-success option to track cvc5's status after each command. When I added implicit define-fun commands for each named term (needed for raw-benchmark), cvc5 started printing spurious ; success messages. This change ended up crashing Kind 2's driver for cvc5. This PR fixes this issue by muting the results of those implicit define-fun commands.
src/parser/smt2/Smt2.g diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/options/named_muted.smt2 [new file with mode: 0644] blob