Running ReqCheck on Linux for testcase generation #769
Description
I tried to run Ultimate ReqCheck to generate a testcase following this example.
https://ultimate-pa.github.io/hanfor/introduction/index.html#test-generation
req file content is:
Input A is bool
Input B is bool
Output H is bool
Output I is bool
Output C is bool
Req1: Globally, it is always the case that if "A" holds, then "H" holds after at most "10" time units
Req2: Globally, it is always the case that if "B" holds, then "I" holds after at most "10" time units
Req3: Globally, it is always the case that if "H && I" holds, then "C" holds after at most "10" time units
i use the following command ./run_complete_analysis.py -gt -o testout example_req.req
the execution of Ultimate fails with the following stack trace:
FATAL L? ?]: The Plugin de.uni_freiburg.informatik.ultimat
e.pea2boogie has thrown an exception:
java.lang.IndexOutOfBoundsException: Index 0 out of bounds for length 0
at java.base/jdk.internal.util.Preconditions.outOfBounds(Preconditions.java:100)
at java.base/jdk.internal.util.Preconditions.outOfBoundsCheckIndex(Preconditions.java:106)
at java.base/jdk.internal.util.Preconditions.checkIndex(Preconditions.java:302)
at java.base/java.util.Objects.checkIndex(Objects.java:385)
at java.base/java.util.ArrayList.set(ArrayList.java:470)
at de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2CauseTrackingPea.transformLocations(
Req2CauseTrackingPea.java:224)
at de.uni_freiburg.informatik.ultimate.pea2boogie.testgen.Req2CauseTrackingPea.transformPea(Req2Ca
useTrackingPea.java:139)
i tried this with the precompiled ReqCheck from GitHub:
https://github.com/ultimate-pa/ultimate/releases/download/v0.3.1/UReqCheck-linux.zip
as well compiled from source both with the same error.
./Ultimate --version
This is Ultimate 0.3.1-dev-35a8436538
This is Ultimate 0.3.1-HEAD-35a8436538-m
Version is 0.3.1
Maximal heap size is set to 4.3GB
Value of java.version is 21.0.9
Value of java.specification.name is Java Platform API Specification
Value of java.specification.vendor is Oracle Corporation
Value of java.specification.version is 21
Value of java.runtime.version is 21.0.9+-nixos
Value of java.vm.name is OpenJDK 64-Bit Server VM
Value of java.vm.vendor is Oracle Corporation
Value of java.vm.version is 21.0.9+-nixos