Fix tests

verus-lang · Feb 21, 2025 · ce4f8e0 · ce4f8e0
1 parent 16c34dd
commit ce4f8e0
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/source/rust_verify_test/tests/external_traits.rs b/source/rust_verify_test/tests/external_traits.rs
@@ -308,9 +308,6 @@ test_verify_one_file_with_options! {
             type ExternalTraitSpecificationFor: Ord;
         }
 
-        #[verifier::external_type_specification]
-        pub struct ExOrdering(core::cmp::Ordering);
-
         #[verifier::external_type_specification]
         #[verifier::external_body]
         #[verifier::reject_recursive_types_in_ground_variants(I)]

diff --git a/source/rust_verify_test/tests/structural.rs b/source/rust_verify_test/tests/structural.rs
@@ -48,7 +48,7 @@ test_verify_one_file! {
             let v2 = Thing { v: true };
             assert_(v1 == v2);
         }
-    } => Err(err) => assert_vir_error_msg(err, "==/!= for non smt equality types")
+    } => Err(err) => assert_vir_error_msg(err, "`core::cmp::PartialEq::eq` is not supported")
 }
 
 test_verify_one_file! {