mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix #4538 - regression when renaming family from special_relations to specrels
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
80cc45c5c1
commit
65e6b73873
|
@ -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<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
|
||||
|
||||
install_tactics(*this);
|
||||
|
|
|
@ -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));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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) {
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue