./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product27_false-assert.jar
--------------------------------------------------------------------------------
./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.AAbHW7.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product27_false-assert.jar
Unwind: 11
JBMC version 5.9 (cbmc-5.7-5176-g7c4b5aa) 64-bit x86_64 linux
Parsing ../git-sv-benchmarks/java/MinePump/spec1-5_product27_false-assert.jar
JAR file without entry point: loading class files
failed to load class `java.io.ObjectOutputStream'
failed to load class `java.io.ObjectInputStream'
failed to load class `java.io.PrintWriter'
failed to load class `java.io.PrintStream'
failed to load class `java.io.IOException'
failed to load class `java.io.Serializable'
failed to load class `java.lang.StackTraceElement'
failed to load class `java.util.Objects'
failed to load class `java.lang.AbstractStringBuilder'
failed to load class `java.lang.invoke.MethodHandles'
failed to load class `java.util.PrimitiveIterator'
failed to load class `java.lang.invoke.LambdaMetafactory'
failed to load class `java.lang.invoke.MethodHandle'
failed to load class `java.lang.invoke.MethodType'
failed to load class `java.lang.invoke.MethodHandles$Lookup'
failed to load class `java.lang.invoke.CallSite'
failed to load class `java.util.Spliterators'
failed to load class `java.util.PrimitiveIterator$OfInt'
failed to load class `java.util.Spliterator$OfInt'
failed to load class `java.util.stream.StreamSupport'
failed to load class `java.util.stream.IntStream'
failed to load class `java.util.Spliterator'
failed to load class `java.util.function.Supplier'
failed to load class `java.util.NoSuchElementException'
failed to load class `java.util.function.IntConsumer'
failed to load class `java.lang.Comparable'
failed to load class `java.util.Locale'
failed to load class `java.lang.CharacterName'
failed to load class `java.lang.CharacterData'
failed to load class `java.lang.Byte'
failed to load class `java.io.UnsupportedEncodingException'
failed to load class `java.util.Comparator'
failed to load class `java.lang.Iterable'
failed to load class `java.util.Iterator'
failed to load class `java.nio.charset.Charset'
failed to load class `java.io.BufferedInputStream'
failed to load class `java.lang.Number'
failed to load class `java.lang.Long'
failed to load class `java.lang.Appendable'
failed to load class `java.util.HashMap'
failed to load class `sun.reflect.Reflection'
failed to load class `java.lang.System'
failed to load class `java.lang.SecurityManager'
failed to load class `java.lang.ClassLoader'
failed to load class `java.util.Map'
failed to load class `java.io.ObjectStreamException'
failed to load class `java.io.InvalidObjectException'
failed to load class `java.util.Arrays'
failed to load class `java.util.stream.DoubleStream'
failed to load class `java.util.stream.LongStream'
Converting
Method: java::java.lang.Object.getClass
could not parse signature: ()Ljava/lang/Class<*>;
Unsupported class signature: wild card generic
reverting to descriptor: ()Ljava/lang/Class;
Method: java::java.lang.String.join
could not parse signature: (Ljava/lang/CharSequence;Ljava/lang/Iterable<+Ljava/lang/CharSequence;>;)Ljava/lang/String;
Unsupported class signature: wild card generic
reverting to descriptor: (Ljava/lang/CharSequence;Ljava/lang/Iterable;)Ljava/lang/String;
Method: java::MinePumpSystem.Environment$WaterLevelEnum.<init>
signature: ()V
descriptor: (Ljava/lang/String;I)V
different number of parameters, reverting to descriptor
Method: java::java.lang.Class.forName
could not parse signature: (Ljava/lang/String;)Ljava/lang/Class<*>;
Unsupported class signature: wild card generic
reverting to descriptor: (Ljava/lang/String;)Ljava/lang/Class;
Method: java::java.lang.Class.forName
could not parse signature: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class<*>;
Unsupported class signature: wild card generic
reverting to descriptor: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class;
Method: java::java.lang.Class.desiredAssertionStatus0
could not parse signature: (Ljava/lang/Class<*>;)Z
Unsupported class signature: wild card generic
reverting to descriptor: (Ljava/lang/Class;)Z
Method: java::java.lang.Character$UnicodeScript.<init>
signature: ()V
descriptor: (Ljava/lang/String;I)V
different number of parameters, reverting to descriptor
Class: java.lang.Enum
could not parse signature: <E:Ljava/lang/Enum<TE;>;>Ljava/lang/Object;Ljava/lang/Comparable<TE;>;Ljava/io/Serializable;
Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum<TE
ignoring that the class is generic
Method: java::java.lang.Enum.valueOf
could not parse signature: <T:Ljava/lang/Enum<TT;>;>(Ljava/lang/Class<TT;>;Ljava/lang/String;)TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: (Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;
Method: java::org.cprover.CProver.nondetWithNull
could not parse signature: <T:Ljava/lang/Object;>()TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNull
could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
could not parse signature: <T:Ljava/lang/Object;>()TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNullForNotModelled
could not parse signature: <T:Ljava/lang/Object;>()TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNullForNotModelled
could not parse signature: <T:Ljava/lang/Object;>()TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: ()Ljava/lang/Object;
Java: added 2278 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 11 object bits, 53 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1 thread 0
Unwinding loop __CPROVER__start.0 iteration 2 thread 0
Unwinding loop __CPROVER__start.0 iteration 3 thread 0
Unwinding loop __CPROVER__start.0 iteration 4 thread 0
Unwinding loop __CPROVER__start.0 iteration 5 thread 0
Unwinding recursion java::Main::clinit_wrapper iteration 1
Unwinding recursion java::Actions::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.MinePump::clinit_wrapper iteration 1
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 1 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 105 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 2 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 105 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 3 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 1 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 2 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0
size of program expression: 45011 steps
simple slicing removed 1 assignments
Generated 393 VCC(s), 28 remaining after simplification
Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier
converting SSA
Running string refinement loop with MiniSAT 2.2.1 without simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
1958383 variables, 6157737 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime decision procedure: 24.1005s
Building error trace
Counterexample:
State 3 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000)
State 4 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
high=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 5 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
normal=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 6 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 7 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
normal_return_value=0 (00000000 00000000 00000000 00000000)
State 8 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
high_return_value=0 (00000000 00000000 00000000 00000000)
State 9 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .isAnnotation=false, .isArray=false,
.isInterface=false, .isSynthetic=false,
.isLocalClass=false, .isMemberClass=false,
.isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 12 thread 0
----------------------------------------------------
this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 13 thread 0
----------------------------------------------------
name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 14 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 15 thread 0
----------------------------------------------------
isArray=false (00000000)
State 16 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 17 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 18 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 19 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 20 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 22 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 24 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isAnnotation=false (00000000)
State 26 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isArray=false (00000000)
State 28 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isInterface=false (00000000)
State 30 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isSynthetic=false (00000000)
State 32 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isLocalClass=false (00000000)
State 34 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isMemberClass=false (00000000)
State 36 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0
----------------------------------------------------
MinePumpSystem.MinePump@class_model.isEnum=false (00000000)
State 39 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 40 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$MinePumpSystem_MinePump$$clinit_already_run=false (0)
State 42 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$1$$clinit_already_run=false (0)
State 43 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 44 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Actions$$clinit_already_run=false (0)
State 45 thread 0
----------------------------------------------------
Actions@class_model={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .isAnnotation=false, .isArray=false,
.isInterface=false, .isSynthetic=false,
.isLocalClass=false, .isMemberClass=false,
.isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 48 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 49 thread 0
----------------------------------------------------
name=&Actions.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 50 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 51 thread 0
----------------------------------------------------
isArray=false (00000000)
State 52 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 53 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 54 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 55 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 56 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 58 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
Actions@class_model.name=&Actions.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 60 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0
----------------------------------------------------
Actions@class_model.isAnnotation=false (00000000)
State 62 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0
----------------------------------------------------
Actions@class_model.isArray=false (00000000)
State 64 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0
----------------------------------------------------
Actions@class_model.isInterface=false (00000000)
State 66 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0
----------------------------------------------------
Actions@class_model.isSynthetic=false (00000000)
State 68 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0
----------------------------------------------------
Actions@class_model.isLocalClass=false (00000000)
State 70 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0
----------------------------------------------------
Actions@class_model.isMemberClass=false (00000000)
State 72 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0
----------------------------------------------------
Actions@class_model.isEnum=false (00000000)
State 74 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=false (0)
State 75 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=false (0)
State 76 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
low=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 77 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$VALUES=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 78 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
low={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=3, .data=low_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 79 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
low_return_value=0 (00000000 00000000 00000000 00000000)
State 80 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
low_constarray={ (char)'l', (char)'o', (char)'w' } ({ 00000000 01101100, 00000000 01101111, 00000000 01110111 })
State 81 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
normal={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=6, .data=normal_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 82 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
normal_constarray={ (char)'n', (char)'o', (char)'r', (char)'m', (char)'a', (char)'l' } ({ 00000000 01101110, 00000000 01101111, 00000000 01110010, 00000000 01101101, 00000000 01100001, 00000000 01101100 })
State 83 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
high={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=high_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
high_constarray={ (char)'h', (char)'i', (char)'g', (char)'h' } ({ 00000000 01101000, 00000000 01101001, 00000000 01100111, 00000000 01101000 })
State 85 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
cleanupTimeShifts=0 (00000000 00000000 00000000 00000000)
State 97 thread 0
----------------------------------------------------
dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 99 thread 0
----------------------------------------------------
dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 100 thread 0
----------------------------------------------------
dynamic_object1.length=2 (00000000 00000000 00000000 00000010)
State 103 thread 0
----------------------------------------------------
dynamic_object1.data=dynamic_2_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 104 thread 0
----------------------------------------------------
dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 109 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 111 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 117 thread 0
----------------------------------------------------
dynamic_object4=dynamic_object4#1 (?)
State 121 thread 0
----------------------------------------------------
dynamic_object4={ } ( })
State 126 thread 0
----------------------------------------------------
dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 127 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 132 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 134 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 140 thread 0
----------------------------------------------------
dynamic_object6=dynamic_object6#1 (?)
State 144 thread 0
----------------------------------------------------
dynamic_object6={ } ( })
State 149 thread 0
----------------------------------------------------
dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 150 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 154 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 157 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 161 thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=true (1)
State 168 file Main.java line 8 function java::Main.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
cleanupTimeShifts=2 (00000000 00000000 00000000 00000010)
State 173 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V bytecode-index 1 thread 0
----------------------------------------------------
arg0i=3 (00000000 00000000 00000000 00000011)
State 174 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 175 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 180 thread 0
----------------------------------------------------
java$$Actions$$clinit_already_run=true (1)
State 188 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 189 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 194 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 195 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 200 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 204 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 211 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 216 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 233 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 238 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.env=null, .p=null, .methAndRunningLastTime=false,
.switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 })
State 240 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::Actions", .cproverMonitorCount=0 },
.env=null, .p=null, .methAndRunningLastTime=false,
.switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 })
State 244 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 250 file Actions.java line 14 function java::Actions.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 252 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object13.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 256 file Actions.java line 10 function java::Actions.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 258 file Actions.java line 11 function java::Actions.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 259 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 9 thread 0
----------------------------------------------------
dynamic_object14={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 })
State 261 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 9 thread 0
----------------------------------------------------
dynamic_object14={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment",
.cproverMonitorCount=0 },
.waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 })
State 265 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 269 file MinePumpSystem/Environment.java line 3 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 271 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object14.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 277 thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1)
State 289 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 291 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 295 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 4 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 296 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 4 thread 0
----------------------------------------------------
arg1a=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 297 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 4 thread 0
----------------------------------------------------
arg2i=0 (00000000 00000000 00000000 00000000)
State 301 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 302 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 303 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
ordinal=0 (00000000 00000000 00000000 00000000)
State 307 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 309 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object15.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 313 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object15.@java.lang.Enum.name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 315 file java/lang/Enum.java line 119 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object15.@java.lang.Enum.ordinal=0 (00000000 00000000 00000000 00000000)
State 325 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 5 thread 0
----------------------------------------------------
low=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 331 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
dynamic_object16={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 333 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
dynamic_object16={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 337 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 338 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 10 thread 0
----------------------------------------------------
arg1a=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 339 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 10 thread 0
----------------------------------------------------
arg2i=1 (00000000 00000000 00000000 00000001)
State 343 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 344 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 345 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
ordinal=1 (00000000 00000000 00000000 00000001)
State 349 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 351 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object16.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 355 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object16.@java.lang.Enum.name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 357 file java/lang/Enum.java line 119 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object16.@java.lang.Enum.ordinal=1 (00000000 00000000 00000000 00000001)
State 367 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 11 thread 0
----------------------------------------------------
normal=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 373 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 12 thread 0
----------------------------------------------------
dynamic_object17={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 375 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 12 thread 0
----------------------------------------------------
dynamic_object17={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum",
.cproverMonitorCount=0 },
.name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })
State 379 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 380 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 16 thread 0
----------------------------------------------------
arg1a=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 381 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 16 thread 0
----------------------------------------------------
arg2i=2 (00000000 00000000 00000000 00000010)
State 385 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 386 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 387 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
ordinal=2 (00000000 00000000 00000000 00000010)
State 391 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 393 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object17.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 397 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object17.@java.lang.Enum.name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 399 file java/lang/Enum.java line 119 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object17.@java.lang.Enum.ordinal=2 (00000000 00000000 00000000 00000010)
State 409 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 17 thread 0
----------------------------------------------------
high=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 411 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 413 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::array[reference]",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 414 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object18.length=3 (00000000 00000000 00000000 00000011)
State 417 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object18.data=dynamic_19_array (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 418 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_19_array={ null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 430 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 23 thread 0
----------------------------------------------------
dynamic_19_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 442 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 27 thread 0
----------------------------------------------------
dynamic_19_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 454 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 31 thread 0
----------------------------------------------------
dynamic_19_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 460 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 32 thread 0
----------------------------------------------------
$VALUES=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 466 file MinePumpSystem/Environment.java line 11 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object14.waterLevel=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 468 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=false (00000000)
State 472 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 12 thread 0
----------------------------------------------------
dynamic_object13.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 476 thread 0
----------------------------------------------------
java$$MinePumpSystem_MinePump$$clinit_already_run=true (1)
State 484 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 485 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 490 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 491 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 496 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 500 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 507 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 512 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
clazz=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 529 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 534 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 14 thread 0
----------------------------------------------------
dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.pumpRunning=false, .systemActive=false,
.env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 536 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 14 thread 0
----------------------------------------------------
dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.MinePump",
.cproverMonitorCount=0 },
.pumpRunning=false, .systemActive=false,
.env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 541 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 542 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 546 file MinePumpSystem/MinePump.java line 21 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 548 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 552 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object20.pumpRunning=false (00000000)
State 554 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object20.systemActive=true (00000001)
State 556 file MinePumpSystem/MinePump.java line 22 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 10 thread 0
----------------------------------------------------
dynamic_object20.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 560 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object13.p=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 563 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 564 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 566 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 567 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 568 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 569 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 573 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 580 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 583 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 585 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 589 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 593 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 595 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object21.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 600 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 604 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 619 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 626 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 629 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 631 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 635 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 639 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 641 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object22.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 646 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 650 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 665 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 672 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 675 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 677 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 681 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 685 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 687 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object23.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 692 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 696 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 711 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 712 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 721 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 724 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 726 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 730 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 734 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 736 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object24.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 741 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 745 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 760 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 767 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 772 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 781 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=true (00000001)
State 793 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 799 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 809 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 815 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 822 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 830 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 838 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 844 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 857 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 867 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 868 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 869 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 870 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 878 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 884 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 888 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 894 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 899 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 905 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 915 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 916 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 917 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 918 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 926 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 932 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 936 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 942 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 947 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 953 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 958 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 965 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 966 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 967 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 968 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 970 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 979 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 985 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 989 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 995 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1000 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1006 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1010 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1024 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1033 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1034 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1036 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1044 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1050 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1055 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1061 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1065 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1079 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1080 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1089 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1090 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1092 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1100 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1106 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1111 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1117 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1121 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1135 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1136 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 1148 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1149 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1150 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1151 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1155 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=2 (00000000 00000000 00000000 00000010)
State 1162 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1165 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object93={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1167 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object93={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1171 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1175 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1177 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object93.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1182 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1186 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1201 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 1208 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1211 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object94={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1213 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object94={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1217 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1221 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1223 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object94.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1228 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1232 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1247 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1254 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1257 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object95={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1259 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object95={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1263 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1267 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1269 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object95.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1274 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1278 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1293 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1294 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1303 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1306 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object96={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1308 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object96={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1312 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1316 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1318 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object96.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1323 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1327 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1342 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1347 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1352 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1357 thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1)
State 1360 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1379 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.values:()[LMinePumpSystem/Environment$WaterLevelEnum; bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1382 thread 0
----------------------------------------------------
dynamic_object98={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 1384 thread 0
----------------------------------------------------
dynamic_object98={ .@java.lang.Object={ .@class_identifier="java::array[reference]",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 1385 thread 0
----------------------------------------------------
dynamic_object98.length=3 (00000000 00000000 00000000 00000011)
State 1388 thread 0
----------------------------------------------------
dynamic_object98.data=dynamic_99_array (00010000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1389 thread 0
----------------------------------------------------
dynamic_99_array={ null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 1393 thread 0
----------------------------------------------------
dynamic_99_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1397 thread 0
----------------------------------------------------
dynamic_99_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1401 thread 0
----------------------------------------------------
dynamic_99_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1421 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object102={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 1423 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object102={ .@java.lang.Object={ .@class_identifier="java::array[int]", .cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 1424 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object102.length=3 (00000000 00000000 00000000 00000011)
State 1427 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object102.data=dynamic_103_array (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1428 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_103_array={ 0, 0, 0 } ({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 })
State 1434 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 3 thread 0
----------------------------------------------------
$SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=&dynamic_object102.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1449 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1461 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 8 thread 0
----------------------------------------------------
dynamic_103_array[2L]=1 (00000000 00000000 00000000 00000001)
State 1477 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 13 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1489 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 15 thread 0
----------------------------------------------------
dynamic_103_array[1L]=2 (00000000 00000000 00000000 00000010)
State 1505 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 20 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1517 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 22 thread 0
----------------------------------------------------
dynamic_103_array[0L]=3 (00000000 00000000 00000000 00000011)
State 1527 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1548 file MinePumpSystem/Environment.java line 38 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 12 thread 0
----------------------------------------------------
dynamic_object14.waterLevel=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1563 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1569 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1579 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1585 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1592 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 1600 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1608 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1614 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1627 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1637 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1638 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1639 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1640 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1648 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1654 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1658 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1664 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1669 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1675 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1685 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1686 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1687 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1688 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1696 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1702 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1706 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1712 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1717 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1723 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1728 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 1735 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1736 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1737 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1738 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1740 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1749 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1755 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1759 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1765 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1770 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1776 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1780 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1794 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 1803 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1804 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1806 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1814 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1820 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1825 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1831 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1835 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1849 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1850 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1859 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1860 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1862 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1870 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1876 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1881 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1887 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1891 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1905 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1906 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1917 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1918 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1919 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1920 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1924 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=3 (00000000 00000000 00000000 00000011)
State 1931 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1934 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object202={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1936 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object202={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1940 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object202.@java.lang.Object.@class_identifier (00011100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1944 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object202.@java.lang.Object.@class_identifier (00011100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1946 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object202.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1951 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object202.@java.lang.Object.@class_identifier (00011100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1955 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object202.@java.lang.Object.@class_identifier (00011100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1970 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 1977 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1980 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object203={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1982 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object203={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1986 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object203.@java.lang.Object.@class_identifier (00011100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1990 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object203.@java.lang.Object.@class_identifier (00011100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1992 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object203.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1997 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object203.@java.lang.Object.@class_identifier (00011100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2001 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object203.@java.lang.Object.@class_identifier (00011100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2016 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 2023 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2026 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object204={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2028 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object204={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2032 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object204.@java.lang.Object.@class_identifier (00011100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2036 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object204.@java.lang.Object.@class_identifier (00011100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2038 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object204.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2043 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object204.@java.lang.Object.@class_identifier (00011100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2047 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object204.@java.lang.Object.@class_identifier (00011100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2062 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 2063 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 2072 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2075 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object205={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2077 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object205={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2081 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2085 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2087 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object205.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2092 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2096 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2111 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 2116 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2121 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2132 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2158 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2163 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2171 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=false (00000000)
State 2183 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2189 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2199 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2205 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2212 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 2220 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2228 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2234 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2247 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2257 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2258 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2259 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2260 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2268 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2274 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2278 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2284 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2289 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2295 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2304 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2305 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2306 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2307 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2315 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2321 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2325 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2331 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2336 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2342 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2346 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 2353 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2354 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2355 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 2356 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2358 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2367 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2373 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2377 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2383 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2388 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2394 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2398 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2412 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 2423 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
dynamic_object296={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } })
State 2425 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
dynamic_object296={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.AssertionError",
.cproverMonitorCount=0 },
.detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } })
State 2429 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00100111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2433 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00100111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2437 file java/lang/Error.java line 58 function java::java.lang.Error.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00100111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2441 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00100111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2443 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2447 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object296.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object296.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00100111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
Violated property:
file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30
assertion at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30
false
VERIFICATION FAILED
EC=10
FALSE