mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix assorted compiler warnings

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-05-16 11:44:58 +01:00
parent 7ae68f003a
commit 6c22edc988
14 changed files with 24 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -719,12 +719,11 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C,
// we create a new Z_p manager, since we'll be changing the input one
zp_manager zp_upm(nm);
zp_upm.set_zp(zpe_upm.m().p());
zp_numeral_manager & zp_nm = zp_upm.m();
// get the U, V, such that A*U + B*V = 1 (mod p)
scoped_mpz_vector U(nm), V(nm), D(nm);
zp_upm.ext_gcd(A.size(), A.c_ptr(), B.size(), B.c_ptr(), U, V, D);
SASSERT(D.size() == 1 && zp_nm.is_one(D[0]));
SASSERT(D.size() == 1 && zp_upm.m().is_one(D[0]));
// we start lifting from (a = p, b = p, r = p)
scoped_mpz_vector A_lifted(nm), B_lifted(nm);