From 2b683941b78e4003b9406a9ec235b1dfabf7d00d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Jan 2024 17:46:23 -0800 Subject: [PATCH] fix #7103 --- src/smt/theory_special_relations.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 6203df103..30eac685d 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -893,11 +893,17 @@ namespace smt { func_decl* memf, *nextf, *connectedf; - std::string member, next, connected_sym; - unsigned index = r.decl()->get_parameter(0).get_int(); - member = "member" + std::to_string(index); - next = "next" + std::to_string(index); - connected_sym = "connected" + std::to_string(index); + std::string member, next, connected_sym, id; + auto const& pa = r.decl()->get_parameter(0); + if (pa.is_int()) + id = std::to_string(pa.get_int()); + else if (pa.is_ast() && is_func_decl(pa.get_ast())) + id = to_func_decl(pa.get_ast())->get_name().str(); + else + throw default_exception("expected an integer or function declaration"); + member = "member" + id; + next = "next" + id; + connected_sym = "connected" + id; { sort* dom[2] = { s, listS }; recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true);