mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix build issue for debug mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-20 17:20:52 +02:00
parent 1827f98851
commit b1893f2a58
6 changed files with 40 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_model.cpp
View file

@ -171,7 +171,7 @@ extern "C" {
mk_c(c)->save_ast_trail(result.get());
*v = of_ast(result.get());
RETURN_Z3_model_eval true;
Z3_CATCH_RETURN(0);
Z3_CATCH_RETURN(false);
}
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m) {

24
src/ast/ast.cpp
View file

@ -169,6 +169,29 @@ bool family_manager::has_family(symbol const & s) const {
return m_families.contains(s);
}
#if 0
static unsigned s_count = 0;
void ast::inc_ref() {
SASSERT(m_ref_count < UINT_MAX);
m_ref_count ++;
if (get_id() == 1) {
s_count++;
if (s_count >= 36530) {
TRACE("rc", tout << "inc_ref " << m_ref_count << "\n";);
}
}
}
void ast::dec_ref() {
SASSERT(m_ref_count > 0);
m_ref_count --;
if (get_id() == 1 && s_count >= 36530) {
TRACE("rc", tout << "dec_ref " << m_ref_count << "\n";);
// IF_VERBOSE(0, verbose_stream() << "dec_rc " << s_count << "\n";);
}
}
#endif
// -----------------------------------
//
// decl_info
@ -1814,7 +1837,6 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);

7
src/ast/ast.h
View file

@ -482,6 +482,7 @@ protected:
void * m_mark2_owner;
#endif
#if 1
void inc_ref() {
SASSERT(m_ref_count < UINT_MAX);
m_ref_count ++;
@ -491,6 +492,12 @@ protected:
SASSERT(m_ref_count > 0);
m_ref_count --;
}
#else
void inc_ref();
void dec_ref();
#endif
ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
DEBUG_CODE({

1
src/sat/sat_ddfw.cpp
View file

@ -569,7 +569,6 @@ namespace sat {
for (literal lit : get_clause(i)) {
if (is_true(lit)) found = true;
}
SASSERT(ci.is_true() == found);
SASSERT(found == !m_unsat.contains(i));
}
// every variable in a false clause is in unsat vars

8
src/smt/smt_case_split_queue.cpp
View file

@ -245,7 +245,7 @@ namespace smt {
void mk_var_eh(bool_var v) override {
expr * n = m_context.bool_var2expr(v);
double act;
if (m_cache.find(n, act))
if (n && m_cache.find(n, act))
m_context.set_activity(v, act);
act_case_split_queue::mk_var_eh(v);
}
@ -255,8 +255,10 @@ namespace smt {
double act = m_context.get_activity(v);
if (act > 0.0) {
expr * n = m_context.bool_var2expr(v);
m_cache.insert(n, act);
m_cache_domain.push_back(n);
if (n) {
m_cache.insert(n, act);
m_cache_domain.push_back(n);
}
}
}
act_case_split_queue::del_var_eh(v);

6
src/util/rlimit.cpp
View file

@ -40,12 +40,14 @@ uint64_t reslimit::count() const {
bool reslimit::inc() {
++m_count;
return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
}
bool reslimit::inc(unsigned offset) {
m_count += offset;
return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
bool r = (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
return r;
}
void reslimit::push(unsigned delta_limit) {