diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 0e18098f383..94b72de36f2 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -631,7 +631,7 @@ void string_dependenciest::output_dot(std::ostream &stream) const const auto node_to_string = [&](const nodet &n) { // NOLINT std::stringstream ostream; if(n.kind == nodet::BUILTIN) - ostream << "builtin_" << n.index; + ostream << builtin_function_nodes[n.index]->name() << n.index; else ostream << '"' << format(string_nodes[n.index].expr) << '"'; return ostream.str(); diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index 9497fcf6c8c..b6e7a7880ee 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -161,6 +161,8 @@ class string_builtin_functiont virtual optionalt eval(const std::function &get_value) const = 0; + virtual std::string name() const = 0; + protected: string_builtin_functiont() = default; }; @@ -212,6 +214,11 @@ class string_concat_char_builtin_functiont std::vector eval( const std::vector &input_value, const std::vector &args_value) const override; + + std::string name() const override + { + return "concat_char"; + } }; /// String inserting a string into another one @@ -247,6 +254,11 @@ class string_insertion_builtin_functiont : public string_builtin_functiont optionalt eval(const std::function &get_value) const override; + std::string name() const override + { + return "insert"; + } + protected: string_insertion_builtin_functiont() = default; }; @@ -263,6 +275,11 @@ class string_concatenation_builtin_functiont final const std::vector &input1_value, const std::vector &input2_value, const std::vector &args_value) const override; + + std::string name() const override + { + return "concat"; + } }; /// String creation from other types