diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 8214b1670..39c3dd607 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -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())