mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
ensure abs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
cbaa16df57
commit
361155685c
|
@ -490,7 +490,7 @@ namespace opt {
|
|||
return *this;
|
||||
rational D(abs(m_coeff));
|
||||
for (auto const& [id, coeff] : m_vars)
|
||||
D = lcm(D, coeff);
|
||||
D = lcm(D, abs(coeff));
|
||||
if (D == 1)
|
||||
return *this;
|
||||
SASSERT(D > 0);
|
||||
|
|
Loading…
Reference in a new issue