mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix alias bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-20 22:38:07 -08:00
parent 9cde4f7e05
commit cd6382f1c8
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/bv_sls_eval.cpp
View file

@ -1039,6 +1039,7 @@ namespace bv {
// x*ta + y*tb = x
auto bw = a.bw;
b.get(y);
if (parity_b > 0)
b.shift_right(y, parity_b);
@ -1047,7 +1048,7 @@ namespace bv {
a.bw = 8 * sizeof(digit_t) * a.nw;
// x = 2 ^ b.bw
a.set_zero(x);
a.set(x, b.bw, true);
a.set(x, bw, true);
a.set_one(ta);
a.set_zero(tb);
@ -1072,8 +1073,8 @@ namespace bv {
a.set(tb, aux); // tb := aux
}
a.bw = b.bw;
a.nw = b.nw;
a.bw = bw;
a.nw = a.nw - 1;
// x*a + y*b = 1
#if Z3DEBUG