From 65e6b73873b5ee44209b0e1ed5d36507e647b024 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jul 2020 14:46:40 -0700 Subject: [PATCH] fix #4538 - regression when renaming family from special_relations to specrels Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- src/ast/reg_decl_plugins.cpp | 4 ++-- src/smt/theory_special_relations.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 91cfa3ab8..488828276 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -102,7 +102,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); - m_special_relations_fid = m().mk_family_id("special_relations"); + m_special_relations_fid = m().mk_family_id("specrels"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); install_tactics(*this); diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 6c88f2503..395104a0d 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -57,7 +57,7 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("pb")))) { m.register_plugin(symbol("pb"), alloc(pb_decl_plugin)); } - if (!m.get_plugin(m.mk_family_id(symbol("special_relations")))) { - m.register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin)); + if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) { + m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin)); } } diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 439c61b26..4a9bbd4af 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -91,7 +91,7 @@ namespace smt { } theory_special_relations::theory_special_relations(context& ctx, ast_manager& m): - theory(ctx, m.mk_family_id("special_relations")), + theory(ctx, m.mk_family_id("specrels")), m_util(m), m_can_propagate(false) { }