From def83ed26edbe786baabfdc760211d8537e10d9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Apr 2023 11:13:37 -0700 Subject: [PATCH] fix #6661 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 16 ++++++++-------- src/ast/special_relations_decl_plugin.cpp | 6 +++++- src/ast/special_relations_decl_plugin.h | 4 +++- 3 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 8fae83b26c6..4187fece6f9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -161,7 +161,7 @@ class parameter { bool is_zstring() const { return get_kind() == PARAM_ZSTRING; } bool is_int(int & i) const { return is_int() && (i = get_int(), true); } - bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), true); } + bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), a && true); } bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); } bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); } bool is_double(double & d) const { return is_double() && (d = get_double(), true); } @@ -180,13 +180,13 @@ class parameter { */ void del_eh(ast_manager & m, family_id fid); - int get_int() const { return std::get(m_val); } - ast * get_ast() const { return std::get(m_val); } - symbol get_symbol() const { return std::get(m_val); } - rational const & get_rational() const { return *std::get(m_val); } - zstring const& get_zstring() const { return *std::get(m_val); } - double get_double() const { return std::get(m_val); } - unsigned get_ext_id() const { return std::get(m_val); } + int get_int() const { SASSERT(is_int()); return std::get(m_val); } + ast * get_ast() const { SASSERT(is_ast()); return std::get(m_val); } + symbol get_symbol() const { SASSERT(is_symbol()); return std::get(m_val); } + rational const & get_rational() const { SASSERT(is_rational()); return *std::get(m_val); } + zstring const& get_zstring() const { SASSERT(is_zstring()); return *std::get(m_val); } + double get_double() const { SASSERT(is_double()); return std::get(m_val); } + unsigned get_ext_id() const { SASSERT(is_external()); return std::get(m_val); } bool operator==(parameter const & p) const; bool operator!=(parameter const & p) const { return !operator==(p); } diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 7ed5e834636..b45778d2f83 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -54,7 +54,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl( case OP_SPECIAL_RELATION_LO: name = m_lo; break; case OP_SPECIAL_RELATION_PLO: name = m_plo; break; case OP_SPECIAL_RELATION_TO: name = m_to; break; - case OP_SPECIAL_RELATION_TC: name = m_tc; break; + case OP_SPECIAL_RELATION_TC: + name = m_tc; + if (num_parameters != 1 || !parameters[0].is_ast() || !is_func_decl(parameters[0].get_ast())) + m_manager->raise_exception("parameter to transitive closure should be a function declaration"); + break; } return m_manager->mk_func_decl(name, arity, domain, range, info); } diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index daff802e781..75b5cb134d2 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -71,11 +71,13 @@ class special_relations_util { ast_manager& m; mutable family_id m_fid; func_decl* mk_rel_decl(func_decl* f, decl_kind k) { + SASSERT(f); parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(fid(), k, 1, &p, 2, f->get_domain(), f->get_range()); } family_id fid() const { - if (null_family_id == m_fid) m_fid = m.get_family_id("specrels"); + if (null_family_id == m_fid) + m_fid = m.get_family_id("specrels"); return m_fid; } public: