My two final year project students presented their final dissertations. Iurii Zamiatin did great work developing e_graph_smt_bv, an SMT solver for the bitvector theory based on the egglog equality saturation library. Then along a parallel thread Luigi Rinaldi built parabit a tool for proving once and for all the correctness of parametric bitvector transformations.