diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 640c82f8a..90c3ec7c0 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1127,7 +1127,7 @@ namespace datalog { // fast_pass(t, n); } */ - if (n.get_signature().size() == 0) + if (n.get_signature().empty()) t.get_udoc().reset(t.get_dm()); else if (m_is_subtract) t.get_udoc().subtract(t.get_dm(), n.get_udoc()); diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index 7cad3b348..a9d31e7d3 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -48,7 +48,7 @@ namespace datalog { virtual udoc_relation * complement(func_decl*) const; virtual void to_formula(expr_ref& fml) const; udoc_plugin& get_plugin() const; - virtual bool fast_empty() const { return !get_signature().empty() && m_elems.is_empty(); } + virtual bool fast_empty() const { return m_elems.is_empty(); } virtual bool empty() const; virtual void display(std::ostream& out) const; virtual bool is_precise() const { return true; }