Replace lifetime_generate with THIR-based erasure (#1792)

 - fixes #834
 - fixes #835
 - fixes #959
 - fixes #1296

Co-authored-by: Chris Hawblitzel <[email protected]>

Author: tjhance

examples/guide/interior_mutability.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use verus_builtin_macros::*;

examples/guide/overflow.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 #[allow(unused_imports)]

examples/state_machines/adder.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use verus_builtin_macros::*;

examples/state_machines/adder_generic.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use vstd::{pervasive::*, *};

examples/state_machines/adder_with_max.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use vstd::{pervasive::*, *};

examples/state_machines/conditional.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use vstd::{pervasive::*, *};

examples/state_machines/maps.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use vstd::map::*;

examples/state_machines/refinement.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use verus_builtin_macros::*;

examples/state_machines/tutorial/counting_to_n_atomic.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 #[allow(unused_imports)]
 use verus_builtin::*;
 use verus_builtin_macros::*;

examples/summer_school/chapter-2-3.rs

@@ -1,4 +1,4 @@
-// rust_verify/tests/example.rs expect-warnings
+// rust_verify/tests/example.rs
 use multiset::*;
 #[allow(unused_imports)]
 use prelude::*;