From 9a8c3f60a3ff556acbd3453f367b8b86ab892362 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 16 Nov 2021 17:31:32 -0800 Subject: [PATCH] Fix binding of quoted symbols in `define-fun` (#7655) Our `DefineFunctionCommand` was binding the string representation of the function symbol including the `|` quotes instead of the symbol without the quotes. This commit fixes the issue. --- src/parser/smt2/smt2.cpp | 2 +- src/smt/command.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/parser/quoted-define-fun.smt2 | 5 +++++ 4 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/parser/quoted-define-fun.smt2 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3c423674a..ad380a31c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -879,7 +879,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) api::Term Smt2::parseOpToExpr(ParseOp& p) { - Debug("parser") << "parseOpToExpr: " << p << std::endl; + Trace("parser") << "parseOpToExpr: " << p << std::endl; api::Term expr; if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull()) { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 83f761428..283925903 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1340,7 +1340,7 @@ void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) bool global = sm->getGlobalDeclarations(); api::Term fun = solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global); - sm->getSymbolTable()->bind(fun.toString(), fun, global); + sm->getSymbolTable()->bind(d_symbol, fun, global); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4aae3899d..7806eb308 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -802,6 +802,7 @@ set(regress_0_tests regress0/parser/linear_arithmetic_err3.smt2 regress0/parser/named-attr-error.smt2 regress0/parser/named-attr.smt2 + regress0/parser/quoted-define-fun.smt2 regress0/parser/shadow_fun_symbol_all.smt2 regress0/parser/shadow_fun_symbol_nirat.smt2 regress0/parser/strings20.smt2 diff --git a/test/regress/regress0/parser/quoted-define-fun.smt2 b/test/regress/regress0/parser/quoted-define-fun.smt2 new file mode 100644 index 000000000..02c3e3d52 --- /dev/null +++ b/test/regress/regress0/parser/quoted-define-fun.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) +(define-fun |def_B definitions| () Bool true) +(assert |def_B definitions|) +(set-info :status sat) +(check-sat) -- 2.30.2