Segmentation fault after (push) with trace enabled due to invalid watch list references

[IamYJLee]

While reviewing the trace functionality, I encountered a segmentation fault triggered by the following command:

./z3 -tr:reinit_clauses_bug examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2

After minimizing the SMT-LIB input, I confirmed that the issue consistently occurs when a (push) command is present:

(declare-const x Int)
(push)
(assert (= x 1))
(check-sat) 
(pop)
(assert (= x 0))
(check-sat)

The segmentation fault occurs at the following code location:

z3/src/ast/ast.h

Line 507 in 2714dc2

unsigned get_id() const { return m_id; }

* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x0)
    frame #0: 0x0000000100108fdc z3`ast::get_id(this=0x0000000000000000) const at ast.h:507:38
   502 	            m_mark1_owner = 0;
   503 	            m_mark2_owner = 0;
   504 	        });
   505 	    }
   506 	public:
-> 507 	    unsigned get_id() const { return m_id; }
   508 	    unsigned get_ref_count() const { return m_ref_count; }
   509 	    ast_kind get_kind() const { return static_cast<ast_kind>(m_kind); }
   510 	    unsigned hash() const { return m_hash; }
   511
   512 	#ifdef Z3DEBUG
Target 0: (z3) stopped.

The segmentation fault occurs because the code attempts to call get_id on a nullptr element from the bool_var2expr_map.
This happens at the following line:

z3/src/smt/smt_literal.cpp

Lines 53 to 63 in 2714dc2

	std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map) {
	if (lit == true_literal)
	out << "true";
	else if (lit == false_literal)
	out << "false";
	else if (lit.sign())
	out << "(not #" << bool_var2expr_map[lit.var()]->get_id() << ")";
	else
	out << "#" << bool_var2expr_map[lit.var()]->get_id();
	return out;
	}

At this point, the index into bool_var2expr_map is derived from the size of m_watches.

z3/src/smt/smt_context_pp.cpp

Lines 139 to 156 in 2714dc2

	void context::display_watch_list(std::ostream & out, literal l) const {
	display_literal(out, l); out << " watch_list:\n";
	watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]);
	watch_list::clause_iterator it = wl.begin_clause();
	watch_list::clause_iterator end = wl.end_clause();
	for (; it != end; ++it) {
	display_clause(out, *it); out << "\n";
	}
	}
	void context::display_watch_lists(std::ostream & out) const {
	unsigned s = m_watches.size();
	for (unsigned l_idx = 0; l_idx < s; l_idx++) {
	literal l = to_literal(l_idx);
	display_watch_list(out, l);
	out << "\n";
	}
	}

Further investigation revealed that entries in bool_var2expr_map are reset to nullptr when the solver backtracks after a (push), as part of the cleanup process for variables introduced after the (push).
This happens here:

z3/src/smt/smt_internalizer.cpp

Lines 961 to 977 in 2714dc2

	void context::undo_mk_bool_var() {
	SASSERT(!m_b_internalized_stack.empty());
	m_stats.m_num_del_bool_var++;
	expr * n = m_b_internalized_stack.back();
	unsigned n_id = n->get_id();
	bool_var v = get_bool_var_of_id(n_id);
	m_bool_var2expr[v] = nullptr;
	TRACE(undo_mk_bool_var, tout << "undo_bool: " << v << "\n" << mk_pp(n, m) << "\n" << "m_bdata.size: " << m_bdata.size()
	<< " m_assignment.size: " << m_assignment.size() << "\n";);
	TRACE(mk_var_bug, tout << "undo_mk_bool: " << v << "\n";);
	// bool_var_data & d = m_bdata[v];
	m_case_split_queue->del_var_eh(v);
	if (is_quantifier(n))
	m_qmanager->del(to_quantifier(n));
	set_bool_var(n_id, null_bool_var);
	m_b_internalized_stack.pop_back();
	}

However, while bool_var entries — such as those in bool_var2expr_map — are cleared appropriately, the associated watch list (m_watches) is not updated accordingly.

As a result, the system later attempts to access bool_var2expr_map using dangling indices derived from m_watches, which may now point to nullptr entries — ultimately causing a segmentation fault when get_id() is called on a null pointer.

I believe simply adding a null check to suppress the crash during logging may not be the ideal solution.
Could you provide any guidance on how this issue might be addressed more appropriately?

I’m interested in fixing this issue. If there’s any context or related code I should look at first, I’d appreciate the guidance.

[NikolajBjorner]

what is the stack?
Is it here:

    void context::reinit_clauses(unsigned num_scopes, unsigned num_bool_vars) {
        TRACE(reinit_clauses_bug, display_watch_lists(tout););

I am unable to reproduce this on my side.
The watch list appears to not be in a consistent state at this point. And the fix is to delete this TRACE line.
The entire reason for reinit_clauses is to ensure that every clause has up-to-date atom mapping
(Atoms = integers, clause atoms = a list of expressions) THe lifetime of expressions align with the life-time of the clause, but the life-time of E-nodes comes with the scope. If the solver backtracks, it deletes atoms that were created beyond the backtrack scope and the E-nodes have to be recreated.

[IamYJLee]

The issue disappears and reappears intermittently when I rebuild Z3.
I'm not yet sure what causes this inconsistency.
Once the issue occurs, it continues to reproduce consistently.

The watch list appears to be in an inconsistent state at this point.
Could this potentially affect solver behavior beyond just logging?