From 051a568564958be1433ff64a98808398c1f6e238 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Fri, 10 Dec 2021 12:44:10 -0600 Subject: [PATCH] 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 | 6 ++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/options/named_muted.smt2 | 6 ++++++ 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/options/named_muted.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8ecf3340f..fe401b369 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1794,8 +1794,10 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr] | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE] { // notify that expression was given a name - PARSER_STATE->preemptCommand( - new DefineFunctionCommand(s, expr.getSort(), expr)); + DefineFunctionCommand* defFunCmd = + new DefineFunctionCommand(s, expr.getSort(), expr); + defFunCmd->setMuted(true); + PARSER_STATE->preemptCommand(defFunCmd); PARSER_STATE->notifyNamedExpression(expr, s); } ; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a51a81b19..fda388832 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -787,6 +787,7 @@ set(regress_0_tests regress0/options/didyoumean.smt2 regress0/options/help.smt2 regress0/options/interactive-mode.smt2 + regress0/options/named_muted.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 diff --git a/test/regress/regress0/options/named_muted.smt2 b/test/regress/regress0/options/named_muted.smt2 new file mode 100644 index 000000000..7026298c6 --- /dev/null +++ b/test/regress/regress0/options/named_muted.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --print-success +; EXPECT: success +; EXPECT: success + +(set-logic UF) +(assert (! true :named t)) -- 2.30.2