mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-14 22:25:30 +00:00
Code Activity

skip other tseitin literals

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-04-26 08:32:09 -07:00
parent c8453d05f9
commit 6420bff843
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_parallel.cpp
View file

@ -131,7 +131,7 @@ namespace smt {
expr_ref e(ctx->bool_var2expr(v), m);
if (!e)
continue;
if (m.is_or(e) || m.is_ite(e))
if (m.is_or(e) || m.is_ite(e) || m.is_and(e) || m.is_iff(e))
continue;
if (ctx->get_assignment(v) != l_undef && ctx->get_assign_level(v) == ctx->m_base_lvl) {
bool is_true = ctx->get_assignment(v) == l_true;
@ -636,8 +636,8 @@ namespace smt {
continue; // skip non-initial atoms if configured to do so
}
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
if (m.is_and(e) || m.is_or(e))
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
if (m.is_and(e) || m.is_or(e) || m.is_ite(e) || m.is_iff(e))
continue;
if (lit.sign())