@@ -2042,7 +2042,7 @@ btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b)
2042
2042
assert (a -> width == b -> width );
2043
2043
2044
2044
BtorSimBitVector * res = 0 , * not_b , * sign_a , * sign_b , * neg_a , * neg_b , * add ;
2045
- BtorSimBitVector * cond_a , * cond_b , * urem , * neg_urem , * add_urem , * add_neg_urem ;
2045
+ BtorSimBitVector * cond_a , * cond_b , * urem , * neg_urem ;
2046
2046
bool a_positive , b_positive ;
2047
2047
2048
2048
if (a -> width == 1 )
@@ -2071,12 +2071,10 @@ btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b)
2071
2071
: btorsim_bv_copy (b );
2072
2072
2073
2073
neg_urem = btorsim_bv_neg (urem );
2074
- add_urem = btorsim_bv_add (urem , add );
2075
- add_neg_urem = btorsim_bv_add (neg_urem , add );
2076
2074
2077
2075
res = a_positive && b_positive ? btorsim_bv_copy (urem )
2078
- : !a_positive && b_positive ? btorsim_bv_copy ( add_neg_urem )
2079
- : a_positive && !b_positive ? btorsim_bv_copy ( add_urem )
2076
+ : !a_positive && b_positive ? btorsim_bv_add ( neg_urem , add )
2077
+ : a_positive && !b_positive ? btorsim_bv_add ( urem , add )
2080
2078
: btorsim_bv_copy (neg_urem );
2081
2079
2082
2080
btorsim_bv_free (sign_a );
@@ -2088,8 +2086,6 @@ btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b)
2088
2086
btorsim_bv_free (urem );
2089
2087
btorsim_bv_free (add );
2090
2088
btorsim_bv_free (neg_urem );
2091
- btorsim_bv_free (add_urem );
2092
- btorsim_bv_free (add_neg_urem );
2093
2089
}
2094
2090
2095
2091
assert (res );
0 commit comments