mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 21:16:02 +00:00
Code Activity

Merge branch 'Z3Prover:master' into parallel-solving

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-04 11:54:34 -07:00 • committed by GitHub
commit c9c3548c46
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 103 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_parallel.cpp
View file

@ -191,6 +191,9 @@ namespace smt {
unsigned sz = pctx.assigned_literals().size();
for (unsigned j = unit_lim[i]; j < sz; ++j) {
literal lit = pctx.assigned_literals()[j];
//IF_VERBOSE(0, verbose_stream() << "(smt.thread " << i << " :unit " << lit << " " << pctx.is_relevant(lit.var()) << ")\n";);
if (!pctx.is_relevant(lit.var()))
continue;
expr_ref e(pctx.bool_var2expr(lit.var()), pctx.m);
if (lit.sign()) e = pctx.m.mk_not(e);
expr_ref ce(tr(e.get()), ctx.m);