[Civl] remove unnecessary modifies in a sample (#985)

boogie-org · Nov 17, 2024 · 6b8fbed · 6b8fbed
1 parent e8b5158
commit 6b8fbed
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/Test/civl/inductive-sequentialization/Gauss.bpl b/Test/civl/inductive-sequentialization/Gauss.bpl
@@ -8,7 +8,6 @@ var {:layer 0,2} x:int;
 atomic action {:layer 1} SUM (n: int)
 refines MAIN' using INV;
 creates ADD;
-modifies x;
 {
   assert n >= 0;
 

diff --git a/Test/civl/inductive-sequentialization/Gauss.bpl.expect b/Test/civl/inductive-sequentialization/Gauss.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 5 verified, 0 errors
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,2 @@

		Boogie program verifier finished with 6 verified, 0 errors
		Boogie program verifier finished with 5 verified, 0 errors