mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Removed debug code

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 11:03:18 +02:00
parent 803018b7c3
commit 598e4ede4e
2 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/seq/seq_nielsen.cpp
View file

@ -264,10 +264,8 @@ namespace seq {
m_constraints.push_back(c);
SASSERT(m_graph.m_literal_if_false);
auto lit = m_graph.m_literal_if_false(c.fml);
if (lit != sat::null_literal) {
std::cout << "External literal " << lit << " in node " << m_id << std::endl;
if (lit != sat::null_literal)
set_external_conflict(lit, c.dep);
}
}
void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@ -3704,7 +3702,6 @@ namespace seq {
if (n->m_conflict_external_literal != sat::null_literal) {
// We know from the outer solver that this literal is assigned false
deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_external_literal));
std::cout << "External literal: " << n->m_conflict_external_literal << std::endl;
if (n->m_conflict_internal)
deps = m_dep_mgr.mk_join(deps, n->m_conflict_internal);
continue;

2
src/smt/theory_nseq.cpp
View file

@ -734,7 +734,7 @@ namespace smt {
set_conflict(eqs, lits);
#ifdef Z3DEBUG
#if 1
#if 0
// Pass constraints to a subsolver to check correctness modulo legacy solver
{
smt_params p;