mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
559c3ca012
commit
c428db0bf2
|
@ -142,7 +142,8 @@ namespace sat {
|
||||||
|
|
||||||
bool lut_finder::extract_lut(clause& c2) {
|
bool lut_finder::extract_lut(clause& c2) {
|
||||||
for (literal l : c2) {
|
for (literal l : c2) {
|
||||||
if (!s.is_visited(l.var())) return false;
|
if (!s.is_visited(l.var()))
|
||||||
|
return false;
|
||||||
}
|
}
|
||||||
if (c2.size() == m_vars.size()) {
|
if (c2.size() == m_vars.size()) {
|
||||||
m_clauses_to_remove.push_back(&c2);
|
m_clauses_to_remove.push_back(&c2);
|
||||||
|
|
Loading…
Reference in a new issue