@@ -339,25 +339,25 @@ void interval_domaint::assume_rec(
339339 cond.id ()==ID_gt || cond.id ()==ID_ge ||
340340 cond.id ()==ID_equal || cond.id ()==ID_notequal)
341341 {
342- assert (cond. operands (). size ()== 2 );
342+ const auto &rel = to_binary_relation_expr (cond);
343343
344344 if (negation) // !x<y ---> x>=y
345345 {
346- if (cond .id ()== ID_lt)
347- assume_rec (cond .op0 (), ID_ge, cond .op1 ());
348- else if (cond .id ()== ID_le)
349- assume_rec (cond .op0 (), ID_gt, cond .op1 ());
350- else if (cond .id ()== ID_gt)
351- assume_rec (cond .op0 (), ID_le, cond .op1 ());
352- else if (cond .id ()== ID_ge)
353- assume_rec (cond .op0 (), ID_lt, cond .op1 ());
354- else if (cond .id ()== ID_equal)
355- assume_rec (cond .op0 (), ID_notequal, cond .op1 ());
356- else if (cond .id ()== ID_notequal)
357- assume_rec (cond .op0 (), ID_equal, cond .op1 ());
346+ if (rel .id () == ID_lt)
347+ assume_rec (rel .op0 (), ID_ge, rel .op1 ());
348+ else if (rel .id () == ID_le)
349+ assume_rec (rel .op0 (), ID_gt, rel .op1 ());
350+ else if (rel .id () == ID_gt)
351+ assume_rec (rel .op0 (), ID_le, rel .op1 ());
352+ else if (rel .id () == ID_ge)
353+ assume_rec (rel .op0 (), ID_lt, rel .op1 ());
354+ else if (rel .id () == ID_equal)
355+ assume_rec (rel .op0 (), ID_notequal, rel .op1 ());
356+ else if (rel .id () == ID_notequal)
357+ assume_rec (rel .op0 (), ID_equal, rel .op1 ());
358358 }
359359 else
360- assume_rec (cond .op0 (), cond .id (), cond .op1 ());
360+ assume_rec (rel .op0 (), rel .id (), rel .op1 ());
361361 }
362362 else if (cond.id ()==ID_not)
363363 {
0 commit comments