diff --git a/tests/gcc.c-torture/instruction_semantics/cmovbe_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovbe_r32_r32.k
new file mode 100644
index 000000000..99f7d1222
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/cmovbe_r32_r32.k
@@ -0,0 +1,11 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVBE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovbe R1:R32, R2:R32,  .Operands) => execinstr (cmovbel R1:R32, R2:R32,  .Operands)
+  ...</k>
+       
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/cmove_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmove_r32_r32.k
new file mode 100644
index 000000000..e2bd115f8
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/cmove_r32_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmove R1:R32, R2:R32,  .Operands) => execinstr (cmovel R1:R32, R2:R32,  .Operands)
+  ...</k>
+       
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovge_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovge_r32_r32.k
new file mode 100644
index 000000000..d7402f787
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/cmovge_r32_r32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVGE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovge R1:R32, R2:R32,  .Operands) => execinstr (cmovgel R1:R32, R2:R32,  .Operands)
+  ...</k>
+       
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovle_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/cmovle_r32_r32.k
new file mode 100644
index 000000000..1a73ecb88
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/cmovle_r32_r32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVLE-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovle R1:R32, R2:R32,  .Operands) => execinstr (cmovlel R1:R32, R2:R32,  .Operands)
+  ...</k>
+       
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/cmovs_r64_r64.k b/tests/gcc.c-torture/instruction_semantics/cmovs_r64_r64.k
new file mode 100644
index 000000000..efd544518
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/cmovs_r64_r64.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module CMOVS-R64-R64
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (cmovs R1:R64, R2:R64,  .Operands) => execinstr (cmovsq R1:R64, R2:R64,  .Operands)
+  ...</k>
+       
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/roll_m32.k b/tests/gcc.c-torture/instruction_semantics/roll_m32.k
new file mode 100644
index 000000000..4103a4a6a
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/roll_m32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module ROLL-M32
+  imports X86-CONFIGURATION
+
+  context execinstr(roll:Opcode HOLE:Mem,  .Operands) [result(MemOffset)]
+  
+  rule <k>
+    execinstr (roll:Opcode  memOffset( MemOff:MInt):MemOffset,  .Operands) => execinstr (roll:Opcode $0x1, memOffset( MemOff:MInt):MemOffset,  .Operands)
+  ...</k>
+             
+ endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/sarb_r8.k b/tests/gcc.c-torture/instruction_semantics/sarb_r8.k
new file mode 100644
index 000000000..30fa9c566
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/sarb_r8.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARB-R8
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarb  R2:R8,  .Operands) => execinstr (sarb $0x1, R2:R8,  .Operands) 
+  ...</k>
+      
+endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/sarl_m32.k b/tests/gcc.c-torture/instruction_semantics/sarl_m32.k
new file mode 100644
index 000000000..087fa4892
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/sarl_m32.k
@@ -0,0 +1,13 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARL-M32
+  imports X86-CONFIGURATION
+
+  context execinstr(sarl:Opcode HOLE:Mem,  .Operands) [result(MemOffset)]
+  
+  rule <k>
+    execinstr (sarl:Opcode memOffset( MemOff:MInt):MemOffset,  .Operands) => execinstr (sarl $0x1, memOffset( MemOff),  .Operands)
+  ...</k>
+
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/sarw_r16.k b/tests/gcc.c-torture/instruction_semantics/sarw_r16.k
new file mode 100644
index 000000000..c08abb4fb
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/sarw_r16.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARW-R16
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarw  R2:R16,  .Operands) => execinstr (sarw $0x1, R2:R16,  .Operands) 
+  ...</k>
+   endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/sarx_r32_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/sarx_r32_r32_r32.k
new file mode 100644
index 000000000..0460b21fe
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/sarx_r32_r32_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SARX-R32-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (sarx R1:R32, R2:R32, R3:R32,  .Operands) => execinstr (sarxl R1, R2, R3,  .Operands)
+  ...</k>
+      
+endmodule
+
diff --git a/tests/gcc.c-torture/instruction_semantics/shrl_r32.k b/tests/gcc.c-torture/instruction_semantics/shrl_r32.k
new file mode 100644
index 000000000..aae1765e9
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/shrl_r32.k
@@ -0,0 +1,12 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRL-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrl R2:R32,  .Operands) => execinstr (shrl $0x1, R2:R32,  .Operands)
+  ...</k>
+  endmodule
+
+
diff --git a/tests/gcc.c-torture/instruction_semantics/shrq_r64.k b/tests/gcc.c-torture/instruction_semantics/shrq_r64.k
new file mode 100644
index 000000000..2f2d51a5c
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/shrq_r64.k
@@ -0,0 +1,10 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRQ-R64
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrq R2:R64,  .Operands) => execinstr (shrq $0x1, R2:R64,  .Operands)
+  ...</k>
+endmodule
diff --git a/tests/gcc.c-torture/instruction_semantics/shrx_r32_r32_r32.k b/tests/gcc.c-torture/instruction_semantics/shrx_r32_r32_r32.k
new file mode 100644
index 000000000..96669a704
--- /dev/null
+++ b/tests/gcc.c-torture/instruction_semantics/shrx_r32_r32_r32.k
@@ -0,0 +1,11 @@
+// Autogenerated using stratification.
+requires "x86-configuration.k"
+
+module SHRX-R32-R32-R32
+  imports X86-CONFIGURATION
+
+  rule <k>
+    execinstr (shrx R1:R32, R2:R32, R3:R32,  .Operands) => execinstr (shrxl R1:R32, R2:R32, R3:R32,  .Operands)
+  ...</k>
+   endmodule
+