diff options
Diffstat (limited to 'src/jib/jib_smt.ml')
| -rw-r--r-- | src/jib/jib_smt.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 7f622f85..5847c99c 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1456,7 +1456,6 @@ let smt_instr ctx = | [rk; addr_size; addr; data_size] -> let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in mem_event @ [define_const ctx id ret_ctyp var] - | _ -> Reporting.unreachable l __POS__ "Bad arguments for __read_mem" end |