mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

continue instead of return

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-07 16:55:30 +01:00
parent c088eb4a26
commit 592791ba34
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/variable_elimination.cpp
View file

@ -330,7 +330,7 @@ namespace polysat {
LOG("lcs: " << fac_eval); LOG("lcs: " << fac_eval);
pdd fac_eval_inv = m.zero(); pdd fac_eval_inv = m.zero();
if (!inv(fac_eval, fac_eval_inv)) if (!inv(fac_eval, fac_eval_inv))
return; continue;
pdd const rest_eval = sub.apply_to(rest); pdd const rest_eval = sub.apply_to(rest);
pdd const vs = -rest_eval * fac_eval_inv; // this is the polynomial that computes v pdd const vs = -rest_eval * fac_eval_inv; // this is the polynomial that computes v