diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp index a5e3e84e1..f035388e1 100644 --- a/src/sat/sat_aig_cuts.cpp +++ b/src/sat/sat_aig_cuts.cpp @@ -293,6 +293,9 @@ namespace sat { void aig_cuts::flush_roots(literal_vector const& to_root, node& n) { bool changed = false; + if (n.is_var()) { + return; + } for (unsigned i = 0; i < n.num_children(); ++i) { literal& lit = m_literals[n.offset() + i]; if (to_root[lit.var()] != lit) { diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h index b9142e7f5..706fd121f 100644 --- a/src/sat/sat_cutset.h +++ b/src/sat/sat_cutset.h @@ -14,6 +14,7 @@ #pragma once #include "util/region.h" #include "util/debug.h" +#include "util/util.h" #include namespace sat {