update unit_lim to the correct value

[stormckey]

In z3's co-processing, the units from every thread will be shared at the end of each round.

z3/src/smt/smt_parallel.cpp

Lines 110 to 138 in 3896e18

	std::function<void(void)> collect_units = [&,this]() {
	for (unsigned i = 0; i < num_threads; ++i) {
	context& pctx = *pctxs[i];
	pctx.pop_to_base_lvl();
	ast_translation tr(pctx.m, ctx.m);
	unsigned sz = pctx.assigned_literals().size();
	for (unsigned j = unit_lim[i]; j < sz; ++j) {
	literal lit = pctx.assigned_literals()[j];
	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);
	if (!unit_set.contains(ce)) {
	unit_set.insert(ce);
	unit_trail.push_back(ce);
	}
	}
	}
	unsigned sz = unit_trail.size();
	for (unsigned i = 0; i < num_threads; ++i) {
	context& pctx = *pctxs[i];
	ast_translation tr(ctx.m, pctx.m);
	for (unsigned j = unit_lim[i]; j < sz; ++j) {
	expr_ref src(ctx.m), dst(pctx.m);
	dst = tr(unit_trail.get(j));
	pctx.assert_expr(dst);
	}
	unit_lim[i] = sz;
	}

The code will share the units indexed from unit_lim[i] to pctxs[i].assigned_literals().size(). However, after the sharing, new unit_lim[i] will be set to unit_trail.size(), which is usually larger than current pctxs[i].assigned_literals().size(). As a result, the units indexed from pctxs[i].assigned_literals().size() to unit_trail.size() will not be shared in the future.

To fix this problem, the new unit_lim[i] should just be the number of current units in this thread(pctxs[i].assigned_literals().size())