mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #5279

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-19 13:31:31 -07:00
parent ec034679ce
commit e0860ea173
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/datatype_decl_plugin.cpp
View file

@ -645,7 +645,6 @@ namespace datatype {
return false;
func_decl* c = get_accessor_constructor(f);
SASSERT(n == 1);
std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n";
if (is_constructor(args[0]))
return to_app(args[0])->get_decl() != c;
return false;

8
src/ast/datatype_decl_plugin.h
View file

@ -103,10 +103,10 @@ namespace datatype {
namespace param_size {
class size {
unsigned m_ref;
unsigned m_ref{ 0 };
public:
size(): m_ref(0) {}
virtual ~size() {}
size() {}
virtual ~size() { }
void inc_ref() { ++m_ref; }
void dec_ref();
static size* mk_offset(sort_size const& s);
@ -197,7 +197,7 @@ namespace datatype {
sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { m_sort_size = p; if (p) p->inc_ref(); m_sort = nullptr; }
void set_sort_size(param_size::size* p) { auto* q = m_sort_size; m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; }
def* translate(ast_translation& tr, util& u);
};