./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product2_false-assert.jar
--------------------------------------------------------------------------------
./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.zs8NxL.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product2_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_product2_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
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 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 Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 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 Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 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
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 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
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 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: 10062 steps
simple slicing removed 1 assignments
Generated 19 VCC(s), 6 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
235976 variables, 511889 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime decision procedure: 0.535647s
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
----------------------------------------------------
normal_return_value=0 (00000000 00000000 00000000 00000000)
State 5 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 6 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 9 thread 0
----------------------------------------------------
this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 10 thread 0
----------------------------------------------------
name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 11 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 12 thread 0
----------------------------------------------------
isArray=false (00000000)
State 13 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 14 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 15 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 16 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 17 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 19 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 (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 21 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 23 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 25 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 27 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 29 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 31 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 33 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 36 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 39 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 40 thread 0
----------------------------------------------------
name=&Actions.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 41 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 42 thread 0
----------------------------------------------------
isArray=false (00000000)
State 43 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 44 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 45 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 46 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 47 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 49 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 (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 51 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 53 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 55 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 57 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 59 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 61 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 63 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 66 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$MinePumpSystem_MinePump$$clinit_already_run=false (0)
State 67 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
cleanupTimeShifts=0 (00000000 00000000 00000000 00000000)
State 69 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 70 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 71 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 72 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 73 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 74 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 75 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 76 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, 00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 77 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 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, 00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 79 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 80 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
high_return_value=0 (00000000 00000000 00000000 00000000)
State 81 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=false (0)
State 82 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Actions$$clinit_already_run=false (0)
State 83 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 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
low_return_value=0 (00000000 00000000 00000000 00000000)
State 85 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 86 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, 00000010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 98 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 100 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 101 thread 0
----------------------------------------------------
dynamic_object1.length=4 (00000000 00000000 00000000 00000100)
State 104 thread 0
----------------------------------------------------
dynamic_object1.data=dynamic_2_array (00000010 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 105 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 110 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 112 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 (00000010 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 118 thread 0
----------------------------------------------------
dynamic_object4=dynamic_object4#1 (?)
State 122 thread 0
----------------------------------------------------
dynamic_object4={ } ( })
State 127 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, 00000010 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 128 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 133 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 135 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 (00000010 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 141 thread 0
----------------------------------------------------
dynamic_object6=dynamic_object6#1 (?)
State 145 thread 0
----------------------------------------------------
dynamic_object6={ } ( })
State 150 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, 00000010 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 151 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 156 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object7={ .@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 158 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_2_array[2L]=&dynamic_object7.@java.lang.Object.@class_identifier (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 164 thread 0
----------------------------------------------------
dynamic_object8=dynamic_object8#1 (?)
State 168 thread 0
----------------------------------------------------
dynamic_object8={ } ( })
State 173 thread 0
----------------------------------------------------
dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=dynamic_object8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000011 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 174 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object7.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 179 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object9={ .@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 181 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_2_array[3L]=&dynamic_object9.@java.lang.Object.@class_identifier (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 187 thread 0
----------------------------------------------------
dynamic_object10=dynamic_object10#1 (?)
State 191 thread 0
----------------------------------------------------
dynamic_object10={ } ( })
State 196 thread 0
----------------------------------------------------
dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=dynamic_object10 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000011 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 197 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object9.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 201 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 204 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 208 thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=true (1)
State 215 file Main.java line 8 function java::Main.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
cleanupTimeShifts=2 (00000000 00000000 00000000 00000010)
State 220 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 221 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 222 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 227 thread 0
----------------------------------------------------
java$$Actions$$clinit_already_run=true (1)
State 235 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 236 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 241 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 (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 242 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 247 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 (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 251 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 258 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 263 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 (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 280 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 285 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 287 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 291 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 297 file Actions.java line 14 function java::Actions.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 299 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 303 file Actions.java line 10 function java::Actions.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 305 file Actions.java line 11 function java::Actions.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 306 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 308 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 312 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 316 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 318 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 324 thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1)
State 336 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 338 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 342 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 343 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 344 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 348 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 349 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 350 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 354 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 356 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 360 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 362 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 372 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 378 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 380 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 384 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 385 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 (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 386 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 390 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 391 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 (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 392 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 396 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 398 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 402 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 (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 404 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 414 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 420 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 422 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 426 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 427 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 (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 428 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 432 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 433 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 (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 434 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 438 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 440 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 444 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 (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 446 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 456 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 458 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 460 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 461 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 464 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
dynamic_object18.data=dynamic_19_array (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 465 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 477 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 489 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 501 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 507 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 (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 513 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 515 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=false (00000000)
State 519 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 523 thread 0
----------------------------------------------------
java$$MinePumpSystem_MinePump$$clinit_already_run=true (1)
State 531 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 (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 532 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 537 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 (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 538 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 543 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 (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 547 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 554 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 559 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 (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 576 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 581 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 583 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 588 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 589 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 593 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 (00000100 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_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 599 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 601 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 603 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 607 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 (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 610 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 (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 611 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 613 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 614 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 615 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 616 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 620 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 627 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 630 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 632 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 636 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 640 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 (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 642 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 647 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 651 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 666 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 673 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 676 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 678 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 682 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 686 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 (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 688 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 693 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 697 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 712 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 719 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 722 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 724 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 728 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 732 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 (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 734 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 739 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 743 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 758 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=1 (00000000 00000000 00000000 00000001)
State 759 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 766 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 771 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 776 thread 0
----------------------------------------------------
java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1)
State 779 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 798 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 (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 801 thread 0
----------------------------------------------------
dynamic_object25={ .@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 803 thread 0
----------------------------------------------------
dynamic_object25={ .@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 804 thread 0
----------------------------------------------------
dynamic_object25.length=3 (00000000 00000000 00000000 00000011)
State 807 thread 0
----------------------------------------------------
dynamic_object25.data=dynamic_26_array (00000101 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 808 thread 0
----------------------------------------------------
dynamic_26_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 812 thread 0
----------------------------------------------------
dynamic_26_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 816 thread 0
----------------------------------------------------
dynamic_26_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 820 thread 0
----------------------------------------------------
dynamic_26_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 840 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object27={ .@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 842 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object27={ .@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 843 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object27.length=3 (00000000 00000000 00000000 00000011)
State 846 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object27.data=dynamic_28_array (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 847 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_28_array={ 0, 0, 0 } ({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 })
State 853 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 3 thread 0
----------------------------------------------------
$SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=&dynamic_object27.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 868 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 880 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 8 thread 0
----------------------------------------------------
dynamic_28_array[2L]=1 (00000000 00000000 00000000 00000001)
State 896 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 908 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 15 thread 0
----------------------------------------------------
dynamic_28_array[1L]=2 (00000000 00000000 00000000 00000010)
State 924 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 936 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 22 thread 0
----------------------------------------------------
dynamic_28_array[0L]=3 (00000000 00000000 00000000 00000011)
State 946 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 967 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 977 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 982 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 991 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=true (00000001)
State 1000 file Main.java line 42 function java::Main.randomSequenceOfActions:(I)V bytecode-index 33 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1006 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1021 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1027 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1037 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1043 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1050 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 1058 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1066 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 (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1076 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1086 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1087 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1088 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1089 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1097 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1103 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1107 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1113 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1118 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1124 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1134 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1135 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1136 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1137 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1145 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1151 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1155 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1161 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1166 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1172 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1177 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 1184 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1185 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1186 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1187 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1189 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1198 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1204 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1208 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1214 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1219 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1225 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1229 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1243 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 1252 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1253 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1255 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1263 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1269 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1274 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1280 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1284 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1298 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1299 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1308 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1309 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1311 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1319 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1325 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1330 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1336 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1340 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1354 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1355 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1366 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1367 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1368 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1369 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1373 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=2 (00000000 00000000 00000000 00000010)
State 1380 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1383 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object30={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1385 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object30={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1389 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1393 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1395 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object30.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1400 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1404 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1419 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 1426 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1429 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object31={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1431 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object31={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1435 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1439 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1441 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object31.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1446 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1450 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1465 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1472 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1475 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1477 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1481 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1485 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1487 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object32.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1492 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1496 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1511 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1512 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1521 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1524 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object33={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1526 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object33={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1530 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1534 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1536 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object33.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1541 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1545 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1560 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1565 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1570 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1581 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1612 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1618 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1628 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1634 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1641 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 1649 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1657 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 (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1667 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1677 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1678 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1679 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1680 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1688 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1694 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1698 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1704 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1709 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1715 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1725 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1726 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1727 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1728 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1736 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1742 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1746 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1752 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1757 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1763 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1768 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 1775 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1776 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1777 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1778 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1780 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1789 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1795 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1799 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1805 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=1 (00000000 00000000 00000000 00000001)
State 1810 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1816 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1820 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1834 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 1843 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1844 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1846 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1854 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1860 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1865 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1871 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1875 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1889 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1890 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1899 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1900 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1902 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1910 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1916 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1921 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1927 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 1931 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1945 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1946 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1957 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 1958 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 1959 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 1960 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 1964 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
anonlocal::2i=3 (00000000 00000000 00000000 00000011)
State 1971 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1974 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object43={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1976 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object43={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 1980 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object43.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1984 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object43.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1986 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object43.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 1991 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object43.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 1995 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object43.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2010 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 2017 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2020 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object44={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2022 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object44={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2026 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object44.@java.lang.Object.@class_identifier (00000111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2030 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object44.@java.lang.Object.@class_identifier (00000111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2032 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object44.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2037 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object44.@java.lang.Object.@class_identifier (00000111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2041 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object44.@java.lang.Object.@class_identifier (00000111 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2056 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 2063 thread 0
----------------------------------------------------
anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2066 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object45={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2068 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object45={ .@java.lang.Object={ .@class_identifier="java::java.util.Random",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 2072 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object45.@java.lang.Object.@class_identifier (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2076 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object45.@java.lang.Object.@class_identifier (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2078 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object45.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2083 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::0a=&dynamic_object45.@java.lang.Object.@class_identifier (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2087 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object45.@java.lang.Object.@class_identifier (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2102 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
anonlocal::5i=1 (00000000 00000000 00000000 00000001)
State 2103 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
anonlocal::6i=0 (00000000 00000000 00000000 00000000)
State 2110 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2115 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2126 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2152 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2157 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2165 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object14.methaneLevelCritical=false (00000000)
State 2174 file Main.java line 42 function java::Main.randomSequenceOfActions:(I)V bytecode-index 33 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2180 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2195 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2201 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2211 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2217 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2224 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object13.switchedOnBeforeTS=false (00000000)
State 2232 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2240 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 (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2250 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2260 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2261 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2262 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2263 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2271 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2277 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2281 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2287 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2292 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2298 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2307 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2308 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2309 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2310 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2318 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2324 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2328 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2334 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2339 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2345 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2349 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
dynamic_object13.methAndRunningLastTime=false (00000000)
State 2356 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2357 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2358 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 2359 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2361 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2370 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2376 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2380 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2386 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 2391 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2397 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 2401 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2415 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
anonlocal::4i=1 (00000000 00000000 00000000 00000001)
State 2426 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
dynamic_object60={ .@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 2428 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
dynamic_object60={ .@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 2432 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0
----------------------------------------------------
this=&dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001000 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2436 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001000 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2440 file java/lang/Error.java line 58 function java::java.lang.Error.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001000 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2444 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001000 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 2446 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 2450 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object60.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object60.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001000 11100000 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