Standard output
736451 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/bigint/Test.java
736451 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.2ns
736452 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
736604 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
736605 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
736606 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
736606 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta
737275 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression
738681 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
741276 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s
741279 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from ../key.ui/examples/heap/vstte10_01_SumAndMax/src/SumAndMax.java
741279 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns
741280 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
744329 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s
744337 INFO Test worker d.u.i.k.s.n.ContractLoadingTests self.sumAndMax(a) catch(exc)
pre: ( \forall int i;
( (0 <= i & i < a.length)<<SC>> & inInt(i)
-> 0 <= a[i])
& ((self.<inv><<impl>> & (!a = null)<<impl>>)<<SC>>))<<SC>>
post: (\forall int i;
( (0 <= i & i < a.length)<<SC>> & inInt(i)
-> a[i] <= self.max)
& (( ( a.length > 0
-> \exists int i;
(( (0 <= i
& i < a.length)<<SC>>
& inInt(i)
& self.max = a[i])<<SC>>))
& (( self.sum = bsum{int i;}(0, a.length, a[i])
& (( self.sum <= a.length * self.max
& self.<inv><<impl>>)<<SC>>))<<SC>>))<<SC>>))<<SC>>
& (exc = null)<<impl>>
mod: {(self, SumAndMax::$sum)}
\cup {(self, SumAndMax::$max)}
termination: diamond
744338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/issues/1658/Test.java
744338 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns
744338 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
747324 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s
747325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/specMath/java/Test.java
747325 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns
747325 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config
748368 DEBUG Test worker d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods.
750719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s