diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml
index 26e7cdabd7..4895a8b723 100644
--- a/spectec/src/backend-interpreter/construct.ml
+++ b/spectec/src/backend-interpreter/construct.ml
@@ -446,17 +446,17 @@ let al_to_int_vbinop : value -> V128Op.ibinop = function
   | CaseV ("ADD", []) -> V128Op.Add
   | CaseV ("SUB", []) -> V128Op.Sub
   | CaseV ("MUL", []) -> V128Op.Mul
-  | CaseV ("MinS", []) -> V128Op.MinS
-  | CaseV ("MINU", []) -> V128Op.MinU
-  | CaseV ("MAXS", []) -> V128Op.MaxS
-  | CaseV ("MAXU", []) -> V128Op.MaxU
-  | CaseV ("AVGRU", []) -> V128Op.AvgrU
-  | CaseV ("ADDSATS", []) -> V128Op.AddSatS
-  | CaseV ("ADDSATU", []) -> V128Op.AddSatU
-  | CaseV ("SUBSATS", []) -> V128Op.SubSatS
-  | CaseV ("SUBSATU", []) -> V128Op.SubSatU
+  | CaseV ("MIN", [CaseV ("S", [])]) -> V128Op.MinS
+  | CaseV ("MIN", [CaseV ("U", [])]) -> V128Op.MinU
+  | CaseV ("MAX", [CaseV ("S", [])]) -> V128Op.MaxS
+  | CaseV ("MAX", [CaseV ("U", [])]) -> V128Op.MaxU
+  | CaseV ("AVGR_U", []) -> V128Op.AvgrU
+  | CaseV ("ADD_SAT", [CaseV ("S", [])]) -> V128Op.AddSatS
+  | CaseV ("ADD_SAT", [CaseV ("U", [])]) -> V128Op.AddSatU
+  | CaseV ("SUB_SAT", [CaseV ("S", [])]) -> V128Op.SubSatS
+  | CaseV ("SUB_SAT", [CaseV ("U", [])]) -> V128Op.SubSatU
   | CaseV ("DOTS", []) -> V128Op.DotS
-  | CaseV ("Q15MULRSATS", []) -> V128Op.Q15MulRSatS
+  | CaseV ("Q15MULR_SAT_S", []) -> V128Op.Q15MulRSatS
   | CaseV ("SWIZZLE", []) -> V128Op.Swizzle
   (*TODO *)
   | CaseV ("Shuffle", [ l ]) -> V128Op.Shuffle (al_to_list al_to_int l)
@@ -1305,16 +1305,16 @@ let al_of_int_vbinop : V128Op.ibinop -> value option = function
   | V128Op.Add -> Some (CaseV ("_VI", [ nullary "ADD" ]))
   | V128Op.Sub -> Some (CaseV ("_VI", [ nullary "SUB" ]))
   | V128Op.Mul -> Some (CaseV ("_VI", [ nullary "MUL" ]))
-  | V128Op.MinS -> Some (CaseV ("_VI", [ nullary "MINS" ]))
-  | V128Op.MinU -> Some (CaseV ("_VI", [ nullary "MINU" ]))
-  | V128Op.MaxS -> Some (CaseV ("_VI", [ nullary "MAXS" ]))
-  | V128Op.MaxU -> Some (CaseV ("_VI", [ nullary "MAXU" ]))
-  | V128Op.AvgrU -> Some (CaseV ("_VI", [ nullary "AVGRU" ]))
-  | V128Op.AddSatS -> Some (CaseV ("_VI", [ nullary "ADDSATS" ]))
-  | V128Op.AddSatU -> Some (CaseV ("_VI", [ nullary "ADDSATU" ]))
-  | V128Op.SubSatS -> Some (CaseV ("_VI", [ nullary "SUBSATS" ]))
-  | V128Op.SubSatU -> Some (CaseV ("_VI", [ nullary "SUBSATU" ]))
-  | V128Op.Q15MulRSatS -> Some (CaseV ("_VI", [ nullary "Q15MULRSATS" ]))
+  | V128Op.MinS -> Some (CaseV ("_VI", [ caseV ("MIN", [nullary "S"]) ]))
+  | V128Op.MinU -> Some (CaseV ("_VI", [ caseV ("MIN", [nullary "U"]) ]))
+  | V128Op.MaxS -> Some (CaseV ("_VI", [ caseV ("MAX", [nullary "S"]) ]))
+  | V128Op.MaxU -> Some (CaseV ("_VI", [ caseV ("MAX", [nullary "U"]) ]))
+  | V128Op.AvgrU -> Some (CaseV ("_VI", [ nullary "AVGR_U" ]))
+  | V128Op.AddSatS -> Some (CaseV ("_VI", [ CaseV ("ADD_SAT", [nullary "S"]) ]))
+  | V128Op.AddSatU -> Some (CaseV ("_VI", [ CaseV ("ADD_SAT", [nullary "U"]) ]))
+  | V128Op.SubSatS -> Some (CaseV ("_VI", [ CaseV ("SUB_SAT", [nullary "S"])]))
+  | V128Op.SubSatU -> Some (CaseV ("_VI", [ CaseV ("SUB_SAT", [nullary "U"])]))
+  | V128Op.Q15MulRSatS -> Some (CaseV ("_VI", [ nullary "Q15MULR_SAT_S" ]))
   | _ -> None
 
 let al_of_float_vbinop : V128Op.fbinop -> value = function
diff --git a/spectec/src/backend-interpreter/numerics.ml b/spectec/src/backend-interpreter/numerics.ml
index 568840d205..a13fa609f9 100644
--- a/spectec/src/backend-interpreter/numerics.ml
+++ b/spectec/src/backend-interpreter/numerics.ml
@@ -590,58 +590,58 @@ let vbinop: numerics =
           match op with
           | CaseV ("ADD", []) -> wrap_vbinop V128.I8x16.add v1 v2
           | CaseV ("SUB", []) -> wrap_vbinop V128.I8x16.sub v1 v2
-          | CaseV ("ADDSATS", []) -> wrap_vbinop V128.I8x16.add_sat_s v1 v2
-          | CaseV ("ADDSATU", []) -> wrap_vbinop V128.I8x16.add_sat_u v1 v2
-          | CaseV ("SUBSATS", []) -> wrap_vbinop V128.I8x16.sub_sat_s v1 v2
-          | CaseV ("SUBSATU", []) -> wrap_vbinop V128.I8x16.sub_sat_u v1 v2
-          | CaseV ("MINS", []) -> wrap_vbinop V128.I8x16.min_s v1 v2
-          | CaseV ("MINU", []) -> wrap_vbinop V128.I8x16.min_u v1 v2
-          | CaseV ("MAXS", []) -> wrap_vbinop V128.I8x16.max_s v1 v2
-          | CaseV ("MAXU", []) -> wrap_vbinop V128.I8x16.max_u v1 v2
-          | CaseV ("AVGRU", []) -> wrap_vbinop V128.I8x16.avgr_u v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I8x16.add_sat_s v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I8x16.add_sat_u v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I8x16.sub_sat_s v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I8x16.sub_sat_u v1 v2
+          | CaseV ("MIN", [CaseV ("S", [])]) -> wrap_vbinop V128.I8x16.min_s v1 v2
+          | CaseV ("MIN", [CaseV ("U", [])]) -> wrap_vbinop V128.I8x16.min_u v1 v2
+          | CaseV ("MAX", [CaseV ("S", [])]) -> wrap_vbinop V128.I8x16.max_s v1 v2
+          | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I8x16.max_u v1 v2
+          | CaseV ("AVGR_U", []) -> wrap_vbinop V128.I8x16.avgr_u v1 v2
           | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op)))
         | "I16", 8L -> (
           match op with
           | CaseV ("ADD", []) -> wrap_vbinop V128.I16x8.add v1 v2
           | CaseV ("SUB", []) -> wrap_vbinop V128.I16x8.sub v1 v2
-          | CaseV ("ADDSATS", []) -> wrap_vbinop V128.I16x8.add_sat_s v1 v2
-          | CaseV ("ADDSATU", []) -> wrap_vbinop V128.I16x8.add_sat_u v1 v2
-          | CaseV ("SUBSATS", []) -> wrap_vbinop V128.I16x8.sub_sat_s v1 v2
-          | CaseV ("SUBSATU", []) -> wrap_vbinop V128.I16x8.sub_sat_u v1 v2
-          | CaseV ("MINS", []) -> wrap_vbinop V128.I16x8.min_s v1 v2
-          | CaseV ("MINU", []) -> wrap_vbinop V128.I16x8.min_u v1 v2
-          | CaseV ("MAXS", []) -> wrap_vbinop V128.I16x8.max_s v1 v2
-          | CaseV ("MAXU", []) -> wrap_vbinop V128.I16x8.max_u v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I16x8.add_sat_s v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I16x8.add_sat_u v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I16x8.sub_sat_s v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I16x8.sub_sat_u v1 v2
+          | CaseV ("MIN", [CaseV ("S", [])]) -> wrap_vbinop V128.I16x8.min_s v1 v2
+          | CaseV ("MIN", [CaseV ("U", [])]) -> wrap_vbinop V128.I16x8.min_u v1 v2
+          | CaseV ("MAX", [CaseV ("S", [])]) -> wrap_vbinop V128.I16x8.max_s v1 v2
+          | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I16x8.max_u v1 v2
           | CaseV ("MUL", []) -> wrap_vbinop V128.I16x8.mul v1 v2
-          | CaseV ("AVGRU", []) -> wrap_vbinop V128.I16x8.avgr_u v1 v2
-          | CaseV ("Q15MULRSATS", []) -> wrap_vbinop V128.I16x8.q15mulr_sat_s v1 v2
+          | CaseV ("AVGR_U", []) -> wrap_vbinop V128.I16x8.avgr_u v1 v2
+          | CaseV ("Q15MULR_SAT_S", []) -> wrap_vbinop V128.I16x8.q15mulr_sat_s v1 v2
           | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op)))
         | "I32", 4L -> (
           match op with
           | CaseV ("ADD", []) -> wrap_vbinop V128.I32x4.add v1 v2
           | CaseV ("SUB", []) -> wrap_vbinop V128.I32x4.sub v1 v2
-          | CaseV ("ADDSATS", []) -> wrap_vbinop V128.I32x4.add_sat_s v1 v2
-          | CaseV ("ADDSATU", []) -> wrap_vbinop V128.I32x4.add_sat_u v1 v2
-          | CaseV ("SUBSATS", []) -> wrap_vbinop V128.I32x4.sub_sat_s v1 v2
-          | CaseV ("SUBSATU", []) -> wrap_vbinop V128.I32x4.sub_sat_u v1 v2
-          | CaseV ("MINS", []) -> wrap_vbinop V128.I32x4.min_s v1 v2
-          | CaseV ("MINU", []) -> wrap_vbinop V128.I32x4.min_u v1 v2
-          | CaseV ("MAXS", []) -> wrap_vbinop V128.I32x4.max_s v1 v2
-          | CaseV ("MAXU", []) -> wrap_vbinop V128.I32x4.max_u v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I32x4.add_sat_s v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I32x4.add_sat_u v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I32x4.sub_sat_s v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I32x4.sub_sat_u v1 v2
+          | CaseV ("MIN", [CaseV ("S", [])]) -> wrap_vbinop V128.I32x4.min_s v1 v2
+          | CaseV ("MIN", [CaseV ("U", [])]) -> wrap_vbinop V128.I32x4.min_u v1 v2
+          | CaseV ("MAX", [CaseV ("S", [])]) -> wrap_vbinop V128.I32x4.max_s v1 v2
+          | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I32x4.max_u v1 v2
           | CaseV ("MUL", []) -> wrap_vbinop V128.I32x4.mul v1 v2
           | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op)))
         | "I64", 2L -> (
           match op with
           | CaseV ("ADD", []) -> wrap_vbinop V128.I64x2.add v1 v2
           | CaseV ("SUB", []) -> wrap_vbinop V128.I64x2.sub v1 v2
-          | CaseV ("ADDSATS", []) -> wrap_vbinop V128.I64x2.add_sat_s v1 v2
-          | CaseV ("ADDSATU", []) -> wrap_vbinop V128.I64x2.add_sat_u v1 v2
-          | CaseV ("SUBSATS", []) -> wrap_vbinop V128.I64x2.sub_sat_s v1 v2
-          | CaseV ("SUBSATU", []) -> wrap_vbinop V128.I64x2.sub_sat_u v1 v2
-          | CaseV ("MINS", []) -> wrap_vbinop V128.I64x2.min_s v1 v2
-          | CaseV ("MINU", []) -> wrap_vbinop V128.I64x2.min_u v1 v2
-          | CaseV ("MAXS", []) -> wrap_vbinop V128.I64x2.max_s v1 v2
-          | CaseV ("MAXU", []) -> wrap_vbinop V128.I64x2.max_u v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I64x2.add_sat_s v1 v2
+          | CaseV ("ADD_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I64x2.add_sat_u v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("S", [])]) -> wrap_vbinop V128.I64x2.sub_sat_s v1 v2
+          | CaseV ("SUB_SAT", [CaseV ("U", [])]) -> wrap_vbinop V128.I64x2.sub_sat_u v1 v2
+          | CaseV ("MIN", [CaseV ("S", [])]) -> wrap_vbinop V128.I64x2.min_s v1 v2
+          | CaseV ("MIN", [CaseV ("U", [])]) -> wrap_vbinop V128.I64x2.min_u v1 v2
+          | CaseV ("MAX", [CaseV ("S", [])]) -> wrap_vbinop V128.I64x2.max_s v1 v2
+          | CaseV ("MAX", [CaseV ("U", [])]) -> wrap_vbinop V128.I64x2.max_u v1 v2
           | CaseV ("MUL", []) -> wrap_vbinop V128.I64x2.mul v1 v2
           | _ -> failwith ("Invalid vibinop: " ^ (Print.string_of_value op)))
         | _ -> failwith "Invalid type for vibinop")