The paper was assessed as a high quality work by most of the reviewers, contributing fast methods for robustness verification of binary neural networks and training robust binary networks. The points of strong criticism were positioning of the contribution wrt to the constraint programming methods. Since one of the main claimed contributions is the speed-up, it was questioned whether such a speed-up can be obtained by just existing methods / solvers. In particular, L168: "We present the first extension to handle the reified cardinality constraints" was criticized. The arguments of the discussion clarified that in modern pseudo-Boolean solvers the same (resp. extended) CDCL methods are used to handle constraints. Cardinality constraints and more generally linear inequality constraints can be handled natively. In particular [Elffersand and Nordstrom "Divide and Conquer: Towards Faster Pseudo-Boolean Solving" 2018] describes propagating such constraints directly without any auxiliary variables, which in the implementation may actually efficiently specialize for 0/1 coefficients. This is more than authors say in L135 about PB solvers. The argument then was that reified cardinality constraints are not significantly more complex as they can be encoded as two inequality constraints e.g. as follows: y = [ \sum_i x_i +b >= 0] can be encoded as y < \sum_i x_i +b n*y >= \sum_i x_i +b -1, where n is the number of variables R2 would expect this to be the baseline and would expect the speed-up measured against this baseline would be not as outstanding. However other reviewers agreed, that from the point of view of the current state of the art on BNN verification, the comparison with previously applied methods is valid. A claim of speeding-up over applicable solvers in general would require more thorough discussion of methods and benchmarking. The authors should address all issues raised by reviewers in the final version to the best of their judgement. In particular include comparisons presented in the rebuttal, relate more densely to the literature on constraint programming and refine the claimed contributions, focusing on the BNN application. As a possible extension, optimization rather than SAT formulation may offer solving for the largest eps such that the verification still holds.