read_verilog -sv sizebits.sv
prep; sat -verify -prove-asserts