Skip to content

Commit e84683e

Browse files
committed
btorsim: fix sra not working
The previous sra implementation wasn't working for negative inputs. The implementation was extracting the wrong sign bit (from b instead of a) and also accidently forgot to use it in the conditional, and used not_a instead.
1 parent 71a2a8e commit e84683e

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

src/btorsim/btorsimbv.c

+4-4
Original file line numberDiff line numberDiff line change
@@ -1736,15 +1736,15 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b)
17361736
assert (a->len == b->len);
17371737
assert (a->width == b->width);
17381738

1739-
BtorSimBitVector *res, *sign_b, *srl1, *srl2, *not_a;
1739+
BtorSimBitVector *res, *sign_a, *srl1, *srl2, *not_a;
17401740

1741-
sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1);
1741+
sign_a = btorsim_bv_slice (a, a->width - 1, a->width - 1);
17421742
srl1 = btorsim_bv_srl (a, b);
17431743
not_a = btorsim_bv_not (a);
17441744
srl2 = btorsim_bv_srl (not_a, b);
1745-
res = btorsim_bv_is_true (not_a) ? btorsim_bv_not (srl2)
1745+
res = btorsim_bv_is_true (sign_a) ? btorsim_bv_not (srl2)
17461746
: btorsim_bv_copy (srl1);
1747-
btorsim_bv_free (sign_b);
1747+
btorsim_bv_free (sign_a);
17481748
btorsim_bv_free (srl1);
17491749
btorsim_bv_free (srl2);
17501750
btorsim_bv_free (not_a);

0 commit comments

Comments
 (0)