fix #6661

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 2, 2023 · def83ed · def83ed
1 parent 5b385bd
commit def83ed
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 10 deletions.
diff --git 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<int>(m_val); }
-    ast * get_ast() const { return std::get<ast*>(m_val); }
-    symbol get_symbol() const { return std::get<symbol>(m_val); }
-    rational const & get_rational() const { return *std::get<rational*>(m_val); }
-    zstring const& get_zstring() const { return *std::get<zstring*>(m_val); }
-    double get_double() const { return std::get<double>(m_val); }
-    unsigned get_ext_id() const { return std::get<unsigned>(m_val); }
+    int get_int() const { SASSERT(is_int()); return std::get<int>(m_val); }
+    ast * get_ast() const { SASSERT(is_ast()); return std::get<ast*>(m_val); }
+    symbol get_symbol() const { SASSERT(is_symbol()); return std::get<symbol>(m_val); }
+    rational const & get_rational() const { SASSERT(is_rational()); return *std::get<rational*>(m_val); }
+    zstring const& get_zstring() const { SASSERT(is_zstring()); return *std::get<zstring*>(m_val); }
+    double get_double() const { SASSERT(is_double()); return std::get<double>(m_val); }
+    unsigned get_ext_id() const { SASSERT(is_external()); return std::get<unsigned>(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
@@ -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
@@ -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: