Add verdict, move to regression folder

schuessf · schuessf · commit e2c3c2954a3c · 2023-02-06T14:03:19.000+01:00
diff --git a/trunk/examples/concurrent/bpl/regression/NonAtomicIncrement_2Threads_Loop.bpl b/trunk/examples/concurrent/bpl/regression/NonAtomicIncrement_2Threads_Loop.bpl
@@ -1,3 +1,4 @@
+//#Safe
 /*
  * 
  *
@@ -13,11 +14,11 @@ modifies x;
 
 implementation ULTIMATE.start()
 {
-    x := 0;
+	x := 0;
 
-    fork 1 fistIncrementProcess();
+	fork 1 fistIncrementProcess();
 	fork 2 secondIncrementProcess();
-    join 1;
+	join 1;
 	join 2;
 	assert x >= 2;
 }

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+//#Safe`
`1`	`2`	`/*`
`2`	`3`	`*`
`3`	`4`	`*`
`@@ -13,11 +14,11 @@ modifies x;`
`13`	`14`
`14`	`15`	`implementation ULTIMATE.start()`
`15`	`16`	`{`
`16`		`- x := 0;`
	`17`	`+ x := 0;`
`17`	`18`
`18`		`- fork 1 fistIncrementProcess();`
	`19`	`+ fork 1 fistIncrementProcess();`
`19`	`20`	`fork 2 secondIncrementProcess();`
`20`		`- join 1;`
	`21`	`+ join 1;`
`21`	`22`	`join 2;`
`22`	`23`	`assert x >= 2;`
`23`	`24`	`}`