small example fix

PrincetonUniversity · Mar 28, 2024 · b2f9b5c · b2f9b5c
1 parent 1d784bf
commit b2f9b5c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/progs/verif_io_mem.v b/progs/verif_io_mem.v
@@ -438,7 +438,7 @@ Proof.
          (read_sum_inner n nums) ;; if (b : bool) then Ret tt else lc' <- read_list stdin 4 ;; read_sum (n + sum_Z nums) lc');
              data_at Ews (tarray tuchar 4) (map Vubyte lc) buf; mem_mgr gv; malloc_token Ews (tarray tuchar 4) buf)).
     + entailer!.
-      { lia. }
+      { tauto. }
     + simpl.
       forward.
       { entailer!.