mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
aig roots
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
607a1b3f99
commit
9064e58665
|
@ -251,6 +251,7 @@ namespace sat {
|
|||
augment_aig0(n, m_cuts[v]);
|
||||
}
|
||||
touch(v);
|
||||
IF_VERBOSE(2, display(verbose_stream() << "add " << head.var() << " == ", n) << "\n");
|
||||
}
|
||||
else if (m_aig[v][0].is_const() || !insert_aux(v, n)) {
|
||||
m_literals.shrink(m_literals.size() - sz);
|
||||
|
|
Loading…
Reference in a new issue