All reviewers were leaning towards acceptance. Unfortunately, in the discussion after the rebuttal it became clear that crucial parts of the paper could not be properly understood e.g. the set S in line 147 is a union of polyhedra whereas it seems that this should be an intersection. Moreover, the notation introduced by the authors (box cap to mean convex hull) was not helpful either. The evaluation is not very helpful as the authors evaluate mainly on non-robust models, whereas the gain on the only robust model (ConvBig) on MNIST is marginal and the same is true for CIFAR-10. It is thus hard to judge how significant the impact of the improved relaxation is for the verification of robust models. On the other hand the reviewers appreciated the idea of k-ReLU relaxation as it can also be used in other verification frameworks. In total this is a borderline paper which requires some improvements in the presentation as well as in the evaluation to judge the paper better.