In environment opts : symbolic_options_computed_opt descr : description instr : NormalInstruction stack_addr_size := 64%N : AddressSize sa := 64%N : AddressSize s : N resize_reg := fun r : REG => some_or (fun _ : symbolic_state => reg_of_index_and_shift_and_bitcount_opt (reg_index r, 0%N, s)%zrange) (fun _ : symbolic_state => error.unimplemented_instruction instr) : REG -> M REG dst : ARG l : list ARG src : ARG l0 : list ARG v : idx src_size : N The term "v" has type "idx" while it is expected to have type "Z".