Repository: aptos-labs/aptos-core (language: python)

Issue:
[Bug][Prover] Support enum for number_operation_analysis
# 🐛 Bug

Need to support expression for enum in number_operation_analysis


Discussion / hints:

Fix patch:
diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs
index cf46163fd3965..a03fc714e1674 100644
--- a/third_party/move/move-model/src/model.rs
+++ b/third_party/move/move-model/src/model.rs
@@ -902,6 +902,11 @@ impl GlobalEnv {
         self.diag(Severity::Error, loc, msg)
     }
 
+    /// Adds a warning to this environment, without notes.
+    pub fn warning(&self, loc: &Loc, msg: &str) {
+        self.diag(Severity::Warning, loc, msg)
+    }
+
     /// Adds an error to this environment, with notes.
     pub fn error_with_notes(&self, loc: &Loc, msg: &str, notes: Vec<String>) {
         self.diag_with_notes(Severity::Error, loc, msg, notes)
diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
index 3917c7de48fa1..d7cfdb3cc53d8 100644
--- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
@@ -354,7 +354,7 @@ impl<'env> StructTranslator<'env> {
     /// Return equality check for the field `f`
     pub fn boogie_field_is_equal(&self, f: &FieldEnv<'_>, sep: &str) -> String {
         let field_sel = boogie_field_sel(f);
-        let bv_flag = self.field_bv_flag(&f.get_id());
+        let bv_flag = self.field_bv_flag(f);
         let field_suffix =
             boogie_type_suffix_bv(self.parent.env, &self.inst(&f.get_type()), bv_flag);
         format!(
@@ -367,7 +367,7 @@ impl<'env> StructTranslator<'env> {
     pub fn boogie_field_is_valid(&self, field: &FieldEnv<'_>, sep: &str) -> String {
         let sel = format!("s->{}", boogie_field_sel(field));
         let ty = &field.get_type().instantiate(self.type_inst);
-        let bv_flag = self.field_bv_flag(&field.get_id());
+        let bv_flag = self.field_bv_flag(field);
         format!(
             "{}{}",
             sep,
@@ -380,11 +380,7 @@ impl<'env> StructTranslator<'env> {
         format!(
             "{}: {}",
             boogie_field_sel(f),
-            self.boogie_type_for_struct_field(
-                &f.get_id(),
-                self.parent.env,
-                &self.inst(&f.get_type())
-            )
+            self.boogie_type_for_struct_field(f, self.parent.env, &self.inst(&f.get_type()))
         )
     }
 
@@ -406,7 +402,7 @@ impl<'env> StructTranslator<'env> {
         for (pos, field_env) in struct_env.get_fields_of_variant(variant).enumerate() {
             let field_name = field_env.get_name().display(env.symbol_pool()).to_string();
             let field_type_name = self.boogie_type_for_struct_field(
-                &field_env.get_id(),
+                &field_env,
                 env,
                 &self.inst(&field_env.get_type()),
             );
@@ -558,7 +554,7 @@ impl<'env> StructTranslator<'env> {
     }
 
     /// Return whether a field involves bitwise operations
-    pub fn field_bv_flag(&self, field_id: &FieldId) -> bool {
+    pub fn field_bv_flag(&self, field_env: &FieldEnv) -> bool {
         let global_state = &self
             .parent
             .env
@@ -567,8 +563,20 @@ impl<'env> StructTranslator<'env> {
         let operation_map = &global_state.struct_operation_map;
         let mid = self.struct_env.module_env.get_id();
         let sid = self.struct_env.get_id();
+        let field_id = if field_env.struct_env.has_variants() {
+            let variant = field_env
+                .get_variant()
+                .expect("each field of enum must have a corresponding variant");
+            let pool = self.struct_env.symbol_pool();
+            FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                pool.string(variant).as_str(),
+                pool.string(field_env.get_name()).as_str(),
+            )))
+        } else {
+            field_env.get_id()
+        };
         if let Some(struct_info) = operation_map.get(&(mid, sid)) {
-            matches!(struct_info.get(field_id), Some(&Bitwise))
+            matches!(struct_info.get(&field_id), Some(&Bitwise))
         } else {
             false
         }
@@ -577,11 +585,11 @@ impl<'env> StructTranslator<'env> {
     /// Return boogie type for a struct
     pub fn boogie_type_for_struct_field(
         &self,
-        field_id: &FieldId,
+        field: &FieldEnv,
         env: &GlobalEnv,
         ty: &Type,
     ) -> String {
-        let bv_flag = self.field_bv_flag(field_id);
+        let bv_flag = self.field_bv_flag(field);
         if bv_flag {
             boogie_bv_type(env, ty)
         } else {
@@ -658,7 +666,7 @@ impl<'env> StructTranslator<'env> {
                         field_name,
                         struct_name,
                         self.boogie_type_for_struct_field(
-                            &field_env.get_id(),
+                            field_env,
                             env,
                             &self.inst(&field_env.get_type())
                         ),
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/mono_analysis.rs b/third_party/move/move-prover/bytecode-pipeline/src/mono_analysis.rs
index 7f7bda844af1c..15ce59a5db5fd 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/mono_analysis.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/mono_analysis.rs
@@ -570,8 +570,16 @@ impl<'a> Analyzer<'a> {
                 .entry(struct_.get_qualified_id())
                 .or_default()
                 .insert(targs.to_owned());
-            for field in struct_.get_fields() {
-                self.add_type(&field.get_type().instantiate(targs));
+            if struct_.has_variants() {
+                for variant in struct_.get_variants() {
+                    for field in struct_.get_fields_of_variant(variant) {
+                        self.add_type(&field.get_type().instantiate(targs));
+                    }
+                }
+            } else {
+                for field in struct_.get_fields() {
+                    self.add_type(&field.get_type().instantiate(targs));
+                }
             }
         }
     }
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs b/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
index e4810482c25ab..2ce2c04e18140 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/number_operation.rs
@@ -277,25 +277,55 @@ impl GlobalNumberOperationState {
         let struct_env = struct_env.module_env.env.get_module(mid).into_struct(sid);
         let mut field_oper_map = BTreeMap::new();
 
-        // TODO(#14349): add support for enum type
+        let update_field_map =
+            |field_ty: Type,
+             field_id: FieldId,
+             field_oper_map: &mut BTreeMap<FieldId, NumOperation>| {
+                let arith_flag = if let Type::Reference(_, tr) = field_ty {
+                    tr.is_number()
+                } else if let Type::Vector(tr) = field_ty {
+                    tr.is_number()
+                } else {
+                    field_ty.is_number()
+                };
+                if arith_flag {
+                    field_oper_map.insert(field_id, Arithmetic);
+                } else {
+                    field_oper_map.insert(field_id, Bottom);
+                }
+            };
+
         if !struct_env.has_variants() {
             for (i, field) in struct_env.get_fields().enumerate() {
                 if field_idx_vec.contains(&i) {
                     field_oper_map.insert(field.get_id(), Bitwise);
                 } else {
-                    let field_ty = field.get_type();
-                    let arith_flag = if let Type::Reference(_, tr) = field_ty {
-                        tr.is_number()
-                    } else if let Type::Vector(tr) = field_ty {
-                        tr.is_number()
-                    } else {
-                        field_ty.is_number()
-                    };
-                    if arith_flag {
-                        field_oper_map.insert(field.get_id(), Arithmetic);
-                    } else {
-                        field_oper_map.insert(field.get_id(), Bottom);
-                    }
+                    update_field_map(field.get_type(), field.get_id(), &mut field_oper_map);
+                }
+            }
+            self.struct_operation_map.insert((mid, sid), field_oper_map);
+        } else {
+            if !field_idx_vec.is_empty() {
+                let loc = if let Some(loc) = &struct_env.get_spec().loc {
+                    loc.clone()
+                } else {
+                    struct_env.get_loc()
+                };
+                // enum does support "pragma bv"
+                struct_env.module_env.env.warning(
+                    &loc,
+                    "pragma bv is currently not support in enum types and will be ignored",
+                );
+            }
+            for variant in struct_env.get_variants() {
+                for field in struct_env.get_fields_of_variant(variant) {
+                    let pool = struct_env.symbol_pool();
+                    let new_field_id =
+                        FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                            pool.string(variant).as_str(),
+                            pool.string(field.get_name()).as_str(),
+                        )));
+                    update_field_map(field.get_type(), new_field_id, &mut field_oper_map);
                 }
             }
             self.struct_operation_map.insert((mid, sid), field_oper_map);
@@ -319,6 +349,19 @@ impl GlobalNumberOperationState {
         }
     }
 
+    pub fn get_num_operation_field(
+        &self,
+        mid: &ModuleId,
+        sid: &StructId,
+        field_id: &FieldId,
+    ) -> &NumOperation {
+        self.struct_operation_map
+            .get(&(*mid, *sid))
+            .expect("struct must have a struct operation state")
+            .get(field_id)
+            .expect("expect to get the state")
+    }
+
     /// Gets the number operation of the given node.
     pub fn get_node_num_oper(&self, node_id: NodeId) -> NumOperation {
         self.get_node_num_oper_opt(node_id)
diff --git a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
index 84a1104b496c8..b5d52ed6b1aed 100644
--- a/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
+++ b/third_party/move/move-prover/bytecode-pipeline/src/number_operation_analysis.rs
@@ -17,7 +17,7 @@ use itertools::Either;
 use move_binary_format::file_format::CodeOffset;
 use move_model::{
     ast::{Exp, ExpData, TempIndex},
-    model::{FunId, GlobalEnv, ModuleId, Parameter},
+    model::{FieldId, FunId, GlobalEnv, ModuleId, Parameter, StructId},
     ty::{PrimitiveType, Type},
 };
 use move_stackless_bytecode::{
@@ -277,14 +277,17 @@ impl<'a> NumberOperationAnalysis<'a> {
                         // Update node for field operation
                         move_model::ast::Operation::Select(mid, sid, field_id)
                         | move_model::ast::Operation::UpdateField(mid, sid, field_id) => {
-                            let field_oper = global_state
-                                .struct_operation_map
-                                .get(&(*mid, *sid))
-                                .unwrap()
-                                .get(field_id)
-                                .unwrap();
+                            let field_oper =
+                                global_state.get_num_operation_field(mid, sid, field_id);
                             global_state.update_node_oper(*id, *field_oper, true);
                         },
+                        move_model::ast::Operation::SelectVariants(mid, sid, field_ids) => {
+                            for field_id in field_ids {
+                                let field_oper =
+                                    global_state.get_num_operation_field(mid, sid, field_id);
+                                global_state.update_node_oper(*id, *field_oper, true);
+                            }
+                        },
                         move_model::ast::Operation::Cast => {
                             // Obtained the updated num_oper of the expression
                             let num_oper = global_state.get_node_num_oper(args[0].node_id());
@@ -702,6 +705,41 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                 }
             },
             Call(id, dests, oper, srcs, _) => {
+                let handle_pack_unpack =
+                    |msid: &ModuleId,
+                     sid: &StructId,
+                     id: &AttrId,
+                     i: usize,
+                     field_id: FieldId,
+                     state: &mut NumberOperationState,
+                     global_state: &mut GlobalNumberOperationState,
+                     temps: &[TempIndex]| {
+                        let current_field_oper =
+                            global_state.get_num_operation_field(msid, sid, &field_id);
+                        let pack_oper = global_state
+                            .get_temp_index_oper(cur_mid, cur_fid, temps[i], baseline_flag)
+                            .unwrap();
+                        if self.check_conflict(current_field_oper, pack_oper) {
+                            self.func_target
+                                .func_env
+                                .module_env
+                                .env
+                                .error(&self.func_target.get_bytecode_loc(*id), CONFLICT_ERROR_MSG);
+                        } else {
+                            let merged = current_field_oper.merge(pack_oper);
+                            if merged != *current_field_oper || merged != *pack_oper {
+                                state.changed = true;
+                            }
+                            *global_state
+                                .get_mut_temp_index_oper(cur_mid, cur_fid, temps[i], baseline_flag)
+                                .unwrap() = merged;
+                            global_state
+                                .struct_operation_map
+                                .get_mut(&(*msid, *sid))
+                                .unwrap()
+                                .insert(field_id, merged);
+                        }
+                    };
                 match oper {
                     BorrowLoc | ReadRef | CastU8 | CastU16 | CastU32 | CastU64 | CastU128
                     | CastU256 => {
@@ -812,38 +850,43 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                             .get_module(*msid)
                             .into_struct(*sid);
                         for (i, field) in struct_env.get_fields().enumerate() {
-                            let current_field_oper = global_state
-                                .struct_operation_map
-                                .get(&(*msid, *sid))
-                                .unwrap()
-                                .get(&field.get_id())
-                                .unwrap();
-                            let pack_oper = global_state
-                                .get_temp_index_oper(cur_mid, cur_fid, srcs[i], baseline_flag)
-                                .unwrap();
-                            if self.check_conflict(current_field_oper, pack_oper) {
-                                self.func_target.func_env.module_env.env.error(
-                                    &self.func_target.get_bytecode_loc(*id),
-                                    CONFLICT_ERROR_MSG,
+                            handle_pack_unpack(
+                                msid,
+                                sid,
+                                id,
+                                i,
+                                field.get_id(),
+                                state,
+                                &mut global_state,
+                                srcs,
+                            );
+                        }
+                    },
+                    // Checking and operations in the struct_operation_map when packing an enum type
+                    PackVariant(msid, sid, variant, _) => {
+                        let struct_env = self
+                            .func_target
+                            .global_env()
+                            .get_module(*msid)
+                            .into_struct(*sid);
+                        for (i, field) in struct_env.get_fields_of_variant(*variant).enumerate() {
+                            let pool = struct_env.symbol_pool();
+                            let new_field_id =
+                                FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                                    pool.string(*variant).as_str(),
+                                    pool.string(field.get_name()).as_str(),
+                                )));
+                            if srcs.len() > i {
+                                handle_pack_unpack(
+                                    msid,
+                                    sid,
+                                    id,
+                                    i,
+                                    new_field_id,
+                                    state,
+                                    &mut global_state,
+                                    srcs,
                                 );
-                            } else {
-                                let merged = current_field_oper.merge(pack_oper);
-                                if merged != *current_field_oper || merged != *pack_oper {
-                                    state.changed = true;
-                                }
-                                *global_state
-                                    .get_mut_temp_index_oper(
-                                        cur_mid,
-                                        cur_fid,
-                                        srcs[i],
-                                        baseline_flag,
-                                    )
-                                    .unwrap() = merged;
-                                global_state
-                                    .struct_operation_map
-                                    .get_mut(&(*msid, *sid))
-                                    .unwrap()
-                                    .insert(field.get_id(), merged);
                             }
                         }
                     },
@@ -855,38 +898,43 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                             .get_module(*msid)
                             .into_struct(*sid);
                         for (i, field) in struct_env.get_fields().enumerate() {
-                            let current_field_oper = global_state
-                                .struct_operation_map
-                                .get(&(*msid, *sid))
-                                .unwrap()
-                                .get(&field.get_id())
-                                .unwrap();
-                            let pack_oper = global_state
-                                .get_temp_index_oper(cur_mid, cur_fid, dests[i], baseline_flag)
-                                .unwrap();
-                            if self.check_conflict(current_field_oper, pack_oper) {
-                                self.func_target.func_env.module_env.env.error(
-                                    &self.func_target.get_bytecode_loc(*id),
-                                    CONFLICT_ERROR_MSG,
+                            handle_pack_unpack(
+                                msid,
+                                sid,
+                                id,
+                                i,
+                                field.get_id(),
+                                state,
+                                &mut global_state,
+                                dests,
+                            );
+                        }
+                    },
+                    // Checking and operations in the struct_operation_map when unpacking an enum
+                    UnpackVariant(msid, sid, variant, _) => {
+                        let struct_env = self
+                            .func_target
+                            .global_env()
+                            .get_module(*msid)
+                            .into_struct(*sid);
+                        for (i, field) in struct_env.get_fields_of_variant(*variant).enumerate() {
+                            let pool = struct_env.symbol_pool();
+                            let new_field_id =
+                                FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                                    pool.string(*variant).as_str(),
+                                    pool.string(field.get_name()).as_str(),
+                                )));
+                            if dests.len() > i {
+                                handle_pack_unpack(
+                                    msid,
+                                    sid,
+                                    id,
+                                    i,
+                                    new_field_id,
+                                    state,
+                                    &mut global_state,
+                                    dests,
                                 );
-                            } else {
-                                let merged = current_field_oper.merge(pack_oper);
-                                if merged != *current_field_oper || merged != *pack_oper {
-                                    state.changed = true;
-                                }
-                                *global_state
-                                    .get_mut_temp_index_oper(
-                                        cur_mid,
-                                        cur_fid,
-                                        dests[i],
-                                        baseline_flag,
-                                    )
-                                    .unwrap() = merged;
-                                global_state
-                                    .struct_operation_map
-                                    .get_mut(&(*msid, *sid))
-                                    .unwrap()
-                                    .insert(field.get_id(), merged);
                             }
                         }
                     },
@@ -894,20 +942,14 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                         let dests_oper = global_state
                             .get_temp_index_oper(cur_mid, cur_fid, dests[0], baseline_flag)
                             .unwrap();
-                        let field_oper = global_state
-                            .struct_operation_map
-                            .get(&(*msid, *sid))
-                            .unwrap()
-                            .get(
-                                &self
-                                    .func_target
-                                    .func_env
-                                    .module_env
-                                    .get_struct(*sid)
-                                    .get_field_by_offset(*offset)
-                                    .get_id(),
-                            )
-                            .unwrap();
+                        let field_id = &self
+                            .func_target
+                            .func_env
+                            .module_env
+                            .get_struct(*sid)
+                            .get_field_by_offset(*offset)
+                            .get_id();
+                        let field_oper = global_state.get_num_operation_field(msid, sid, field_id);
 
                         if self.check_conflict(dests_oper, field_oper) {
                             self.func_target
@@ -938,6 +980,67 @@ impl<'a> TransferFunctions for NumberOperationAnalysis<'a> {
                                 );
                         }
                     },
+                    GetVariantField(msid, sid, variants, _, offset)
+                    | BorrowVariantField(msid, sid, variants, _, offset) => {
+                        let struct_env = self
+                            .func_target
+                            .global_env()
+                            .get_module(*msid)
+                            .into_struct(*sid);
+                        let pool = struct_env.symbol_pool();
+                        let field_name = &self
+                            .func_target
+                            .func_env
+                            .module_env
+                            .get_struct(*sid)
+                            .get_field_by_offset_optional_variant(Some(variants[0]), *offset)
+                            .get_name();
+                        let new_field_id =
+                            FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                                pool.string(variants[0]).as_str(),
+                                pool.string(*field_name).as_str(),
+                            )));
+                        let dests_oper = global_state
+                            .get_temp_index_oper(cur_mid, cur_fid, dests[0], baseline_flag)
+                            .unwrap();
+                        let field_oper =
+                            global_state.get_num_operation_field(msid, sid, &new_field_id);
+
+                        if self.check_conflict(dests_oper, field_oper) {
+                            self.func_target
+                                .func_env
+                                .module_env
+                                .env
+                                .error(&self.func_target.get_bytecode_loc(*id), CONFLICT_ERROR_MSG);
+                        } else {
+                            let merged_oper = dests_oper.merge(field_oper);
+                            if merged_oper != *field_oper || merged_oper != *dests_oper {
+                                state.changed = true;
+                            }
+                            *global_state
+                                .get_mut_temp_index_oper(cur_mid, cur_fid, dests[0], baseline_flag)
+                                .unwrap() = merged_oper;
+                            for variant in variants {
+                                let field_name = &self
+                                    .func_target
+                                    .func_env
+                                    .module_env
+                                    .get_struct(*sid)
+                                    .get_field_by_offset_optional_variant(Some(*variant), *offset)
+                                    .get_name();
+                                let new_field_id =
+                                    FieldId::new(pool.make(&FieldId::make_variant_field_id_str(
+                                        pool.string(*variant).as_str(),
+                                        pool.string(*field_name).as_str(),
+                                    )));
+                                global_state
+                                    .struct_operation_map
+                                    .get_mut(&(*msid, *sid))
+                                    .unwrap()
+                                    .insert(new_field_id, merged_oper);
+                            }
+                        }
+                    },
                     Function(msid, fsid, _) => {
                         let module_env = &self.func_target.global_env().get_module(*msid);
                         // Vector functions are handled separately


Test patch:
diff --git a/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.exp b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.exp
new file mode 100644
index 0000000000000..03bbabe471ab8
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.exp
@@ -0,0 +1,12 @@
+Move prover returns: exiting with model building errors
+error: unsupported language construct
+   ┌─ tests/sources/functional/bitwise_operators_enum.move:39:5
+   │
+39 │     enum A has copy, drop {
+   │     ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+   ┌─ tests/sources/functional/bitwise_operators_enum.move:47:5
+   │
+47 │     enum B has drop {
+   │     ^^^^ Move 2 language construct is not enabled: enum types
diff --git a/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.move b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.move
new file mode 100644
index 0000000000000..fbf48422c4422
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.move
@@ -0,0 +1,62 @@
+// exclude_for: cvc5
+address 0x123 {
+
+  module M {
+
+    public fun foo(): u64 {
+      let a = A::VA {
+        f1: 1
+      };
+      spec {
+          assert (int2bv(a.f1) as u64) == (1 as u64);
+      };
+      let b = B::VB {
+        a: a
+      };
+      let c = C {
+        a: 1,
+        b: b.a.f1
+      };
+      let x = (a.f1 & 0)  | (b.a.f1 & 1) | (c.b ^ 2);
+      spec {
+        assert x == (((((1 as u64) & (0 as u64)) as u64) | (((1 as u64) & (1 as u64)) as u64) as u64) | (((1 as u64) ^ (2 as u64)) as u64) as u64);
+      };
+      let _b = B::VB2 {
+        a: a,
+        a2: 2
+      };
+      spec {
+         assert (((int2bv(_b.a.f1) as u64) & (1 as u64)) as u64) == (1 as u64);
+      };
+      x
+    }
+
+    spec foo {
+      pragma bv_ret=b"0";
+      ensures result == (((((1 as u64) & (0 as u64)) as u64) | (((1 as u64) & (1 as u64)) as u64) as u64) | (((1 as u64) ^ (2 as u64)) as u64) as u64);
+    }
+
+    enum A has copy, drop {
+      VA {f1: u64}
+    }
+
+    spec A {
+      pragma bv=b"1"; // this leads to a warning
+    }
+
+    enum B has drop {
+      VB {a: A}
+      VB2 {a: A, a2: u64}
+    }
+
+    struct C has drop {
+      a: u64,
+      b: u64
+    }
+    spec C {
+      pragma bv=b"1";
+    }
+
+  }
+
+}
diff --git a/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.v2_exp b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.v2_exp
new file mode 100644
index 0000000000000..4749b3b8711cc
--- /dev/null
+++ b/third_party/move/move-prover/tests/sources/functional/bitwise_operators_enum.v2_exp
@@ -0,0 +1,7 @@
+warning: pragma bv is currently not support in enum types and will be ignored
+   ┌─ tests/sources/functional/bitwise_operators_enum.move:43:5
+   │
+43 │ ╭     spec A {
+44 │ │       pragma bv=b"1"; // this leads to a warning
+45 │ │     }
+   │ ╰─────^