are our responses to individual reviewers: 2 Reviewer # 1

We thank the reviewers for providing those helpful comments, especially during the challenging time this year. All the empirical results are for small examples (CIF AR-10) raising the question of scalability. We cite previous work on SA T solver support for cardinality constraints (Liffiton et al. [35]) and are happy There are more compact and efficient encodings for encoding cardinality constraints compared to sequential counters. We use sequential counters only for comparison with other BNN verification research (e.g. The main contribution of the paper is the extension of an existing SAT solver (i.e., MiniSAT) to a SAT solver that can Icarte et al. 2019 focuses on generalizability in few-shot learning, which is a different setting than ours.