@@ -141,19 +141,19 @@ bool SSE::handleNonBranch(const IntraCFGEdge* edge) {
141
141
addToSolver (res == op0 % op1);
142
142
break ;
143
143
case BinaryOperator::Xor:
144
- addToSolver (int2bv ( 32 , res) == (int2bv (32 , op0) ^ int2bv (32 , op1)));
144
+ addToSolver (res == bv2int (int2bv (32 , op0) ^ int2bv (32 , op1), 1 ));
145
145
break ;
146
146
case BinaryOperator::And:
147
- addToSolver (int2bv ( 32 , res) == (int2bv (32 , op0) & int2bv (32 , op1)));
147
+ addToSolver (res == bv2int (int2bv (32 , op0) & int2bv (32 , op1), 1 ));
148
148
break ;
149
149
case BinaryOperator::Or:
150
- addToSolver (int2bv ( 32 , res) == (int2bv (32 , op0) | int2bv (32 , op1)));
150
+ addToSolver (res == bv2int (int2bv (32 , op0) | int2bv (32 , op1), 1 ));
151
151
break ;
152
152
case BinaryOperator::AShr:
153
- addToSolver (int2bv ( 32 , res) == ashr (int2bv (32 , op0), int2bv (32 , op1)));
153
+ addToSolver (res == bv2int ( ashr (int2bv (32 , op0), int2bv (32 , op1)), 1 ));
154
154
break ;
155
155
case BinaryOperator::Shl:
156
- addToSolver (int2bv ( 32 , res) == shl (int2bv (32 , op0), int2bv (32 , op1)));
156
+ addToSolver (res == bv2int ( shl (int2bv (32 , op0), int2bv (32 , op1)), 1 ));
157
157
break ;
158
158
default :
159
159
assert (false && " implement this part" );
0 commit comments