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.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3c423674a15a3009628ac2555f061261d6d4d759..ad380a31c730eec8320963f885d4f3699c19d262 100644 (file)
--- 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 83f7614282629f58a5970558f436017a2775f91c..283925903269f1b2a9cc06ee6b77a9619e7f2245 100644 (file)
--- 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 4aae3899dc0e689a40bceff88b7332b766533952..7806eb308d9e07ba95cc4c24e369a1d74b97dd1c 100644 (file)
--- 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 (file)
index 0000000..02c3e3d
--- /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)