diff --git a/examples/Benchmarks/i2c_11.sv b/examples/Benchmarks/i2c_11.sv
index f8b6a1612..ef9d33559 100644
--- a/examples/Benchmarks/i2c_11.sv
+++ b/examples/Benchmarks/i2c_11.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 4500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_12.sv b/examples/Benchmarks/i2c_12.sv
index 7e3e52b03..c9c510102 100644
--- a/examples/Benchmarks/i2c_12.sv
+++ b/examples/Benchmarks/i2c_12.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 5000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1	|| stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_13.sv b/examples/Benchmarks/i2c_13.sv
index bb8044cee..83274daee 100644
--- a/examples/Benchmarks/i2c_13.sv
+++ b/examples/Benchmarks/i2c_13.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 5500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_14.sv b/examples/Benchmarks/i2c_14.sv
index 7fa750fbc..bb82e997b 100644
--- a/examples/Benchmarks/i2c_14.sv
+++ b/examples/Benchmarks/i2c_14.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 6000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_15.sv b/examples/Benchmarks/i2c_15.sv
index 4ebb92885..208599f50 100644
--- a/examples/Benchmarks/i2c_15.sv
+++ b/examples/Benchmarks/i2c_15.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 6500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_16.sv b/examples/Benchmarks/i2c_16.sv
index cd1e5739f..a5627f36b 100644
--- a/examples/Benchmarks/i2c_16.sv
+++ b/examples/Benchmarks/i2c_16.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 7000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_17.sv b/examples/Benchmarks/i2c_17.sv
index f867667c4..af63252e5 100644
--- a/examples/Benchmarks/i2c_17.sv
+++ b/examples/Benchmarks/i2c_17.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 10000, localparam CBITS = 16) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_18.sv b/examples/Benchmarks/i2c_18.sv
index 2da846bd7..cff9016f4 100644
--- a/examples/Benchmarks/i2c_18.sv
+++ b/examples/Benchmarks/i2c_18.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 17500, localparam CBITS = 17) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_19.sv b/examples/Benchmarks/i2c_19.sv
index cdfdd0c0c..7323a3e06 100644
--- a/examples/Benchmarks/i2c_19.sv
+++ b/examples/Benchmarks/i2c_19.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 35000, localparam CBITS = 18) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_20.sv b/examples/Benchmarks/i2c_20.sv
index 5433eb7ad..48896d046 100644
--- a/examples/Benchmarks/i2c_20.sv
+++ b/examples/Benchmarks/i2c_20.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 70000, localparam CBITS = 19) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_3.sv b/examples/Benchmarks/i2c_3.sv
index eda54f1a7..4b44e18db 100644
--- a/examples/Benchmarks/i2c_3.sv
+++ b/examples/Benchmarks/i2c_3.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 500, localparam CBITS = 11) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_4.sv b/examples/Benchmarks/i2c_4.sv
index 93af7eecd..f5daec759 100644
--- a/examples/Benchmarks/i2c_4.sv
+++ b/examples/Benchmarks/i2c_4.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 1000, localparam CBITS = 12) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_5.sv b/examples/Benchmarks/i2c_5.sv
index 2a33e8e9e..043f5c482 100644
--- a/examples/Benchmarks/i2c_5.sv
+++ b/examples/Benchmarks/i2c_5.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 1500, localparam CBITS = 13) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_6.sv b/examples/Benchmarks/i2c_6.sv
index 437f796de..7686e0147 100644
--- a/examples/Benchmarks/i2c_6.sv
+++ b/examples/Benchmarks/i2c_6.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 2000, localparam CBITS = 13) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_7.sv b/examples/Benchmarks/i2c_7.sv
index cdb48bb7e..e06208668 100644
--- a/examples/Benchmarks/i2c_7.sv
+++ b/examples/Benchmarks/i2c_7.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 2500, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_8.sv b/examples/Benchmarks/i2c_8.sv
index 4b9960de5..cd775fa39 100644
--- a/examples/Benchmarks/i2c_8.sv
+++ b/examples/Benchmarks/i2c_8.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 3000, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file
diff --git a/examples/Benchmarks/i2c_9.sv b/examples/Benchmarks/i2c_9.sv
index 089a8d6d6..4c31b8f6a 100644
--- a/examples/Benchmarks/i2c_9.sv
+++ b/examples/Benchmarks/i2c_9.sv
@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 3500, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	p1: assert property  (@(posedge clk) s_eventually (rst == 1 || scl_not_ena == 1 || stretch == 1)) ;
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 endmodule
\ No newline at end of file