mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #7449
This commit is contained in:
parent
879bb4b1f0
commit
30ad22a4ef
|
@ -370,9 +370,14 @@ extern "C" {
|
|||
return;
|
||||
}
|
||||
|
||||
for (expr * e : ctx->assertions()) {
|
||||
to_optimize_ptr(opt)->add_hard_constraint(e);
|
||||
}
|
||||
auto o = to_optimize_ptr(opt);
|
||||
|
||||
for (auto const& [asr, an] : ctx->tracked_assertions())
|
||||
if (an)
|
||||
o->add_hard_constraint(asr, an);
|
||||
else
|
||||
o->add_hard_constraint(asr);
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue