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