Issue 509 slow tests

[Vescatur]

This pull request ensures that the slow tests are run each time a pull request is accepted.
In this commit the slow tests are run. https://github.com/utwente-fmt/vercors/runs/2840658941 Note that problem fail test also ran but that part has been removed from the ci.

One of the tests can be fixed by code from Bob. #509 (comment) However I did not include this code because the scope of the pull request is to run the slow tests. It is not the goal to fix all the tests. It would also cause me to be the author of code which Bob has wrote. I would suggest that Bob makes a pull request to fix this example.

[bobismijnnaam]

monotonicbool.pvl should work by now, could you double check if does, and if so remove it from the problem-fail suite? The rest looks great, nice work.

[Vescatur]

monotonicbool.pvl

unfortunatly not. This is the output.

[progress] [84%] generateQuantifierTriggers took 31 ms
Pass generateQuantifierTriggers did not remove QuantifierWithoutTriggers:
== Example 1: BindingExpression ==
(\exists int i;0 <= i && i < | xs |;xs [ i ])
=== examples\known-problems\parallel\monotonicBool.pvl ===
  42   seq<boolean> toSeq(boolean[] xs) = toSeqImpl(xs, 0);
  43 
                         [--------------------------------
  44   ensures \result == (\exists int i = 0..|xs|; xs[i]);
                          --------------------------------]
  45   boolean foldOr(seq<boolean> xs) =
  46     |xs| > 0 
-----------------------------------------
  Originating here ^
=========================================


== Example 2: BindingExpression ==
(\exists int i;0 <= i && i < N;VCTArray<CT:Ref>.loc(VCTOption<T:VCTArray<CT:Ref>>.getVCTOption1(diz.C_contrib),i).Boolean__item)
=== examples\known-problems\parallel\monotonicBool.pvl ===
  83     }
  84 
                    [----------------------------------
  85     assert b == (\exists int i = 0..N; contrib[i]);
                     ----------------------------------]
  86   }
  87 }
-----------------------------------------
  Originating here ^
=========================================


[progress] [88%] scaleAllPredicateApplications took 15 ms
[progress] [92%] collectInnerDeclarations took 0 ms
[progress] [96%] collectDeclarations took 0 ms
[progress] verifying with builtin silicon backend
[progress] conversion took 78ms
Errors! (1)
=== examples\known-problems\parallel\monotonicBool.pvl ===
  65         ** b == foldOr(toSeq(contrib))
  66         ) {
          [-------------------
  67       par(int tid = 0..N)
  68         context N > 0;
  69         context Perm(contrib, read) ** contrib != null;
  70         context Perm(contrib[tid], 1\2);
  71       {
  72         if (p(tid)) {
  73           // Models: atomic_set(b);
  74           atomic(inv) {
  75             b = true;
  76             contrib[tid] = true;
  77             // Fails:
  78             // b = false;
  79             // contrib[tid] = false;
  80           }
  81         }
  82       }
     -------]
  83     }
  84 
-----------------------------------------
  CallPreCondition:InsufficientPermission
=========================================
=== examples\known-problems\parallel\monotonicBool.pvl ===
  67       par(int tid = 0..N)
  68         context N > 0;
                         [-------
  69         context Perm(contrib, read) ** contrib != null;
                          -------]
  70         context Perm(contrib[tid], 1\2);
  71       {
-----------------------------------------
  caused by
=========================================
[progress] task Viper verification took 5608 ms
The final verdict is Fail
[progress] entire run took 16923 ms

Process finished with exit code 0

[sonarcloud]

Kudos, SonarCloud Quality Gate passed!

0 Bugs
0 Vulnerabilities
0 Security Hotspots
0 Code Smells

71.7% Coverage
0.0% Duplication

[bobismijnnaam]

Okay, I've handled monotonicBool in the problem-fail PR. I'll also review this PR.

[bobismijnnaam]

Looks good. Quite a few new problem-fails we'll have to look at why they are broken...