mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #7103

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-27 17:46:23 -08:00
parent f8a3b6f521
commit 2b683941b7
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_special_relations.cpp
View file

@ -893,11 +893,17 @@ namespace smt {
func_decl* memf, *nextf, *connectedf; func_decl* memf, *nextf, *connectedf;
std::string member, next, connected_sym; std::string member, next, connected_sym, id;
unsigned index = r.decl()->get_parameter(0).get_int(); auto const& pa = r.decl()->get_parameter(0);
member = "member" + std::to_string(index); if (pa.is_int())
next = "next" + std::to_string(index); id = std::to_string(pa.get_int());
connected_sym = "connected" + std::to_string(index); 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 }; sort* dom[2] = { s, listS };
recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true); recfun::promise_def mem = p.ensure_def(symbol(member), 2, dom, m.mk_bool_sort(), true);