mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-07 02:45:19 +00:00
Code Activity

fix #9309

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-23 11:07:16 -07:00
parent f37f87422a
commit 101a9233bc
1 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/util/mpq.cpp
View file

@ -289,6 +289,25 @@ void mpq_manager<SYNCH>::power(mpq const & a, unsigned p, mpq & b) {
set(b, 1);
return;
}
if (eq(a, 1)) {
set(b, 1);
return;
}
if (eq(a, -1)) {
if (p % 2 == 0)
set(b, 1);
else
set(b, -1);
return;
}
if (eq(a, 0)) {
set(b, 0);
return;
}
if (p > (1 << 20))
throw default_exception("power is too large to compute");
unsigned mask = 1;
mpq power;
set(power, a);