./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product4_false-assert.jar


--------------------------------------------------------------------------------


./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.Lb3vHJ.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product4_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_product4_false-assert.jar
JAR file without entry point: loading class files
failed to load class `java.io.ObjectOutputStream'
failed to load class `java.io.ObjectInputStream'
failed to load class `java.io.PrintWriter'
failed to load class `java.io.PrintStream'
failed to load class `java.io.IOException'
failed to load class `java.io.Serializable'
failed to load class `java.lang.StackTraceElement'
failed to load class `java.util.Objects'
failed to load class `java.lang.AbstractStringBuilder'
failed to load class `java.lang.invoke.MethodHandles'
failed to load class `java.util.PrimitiveIterator'
failed to load class `java.lang.invoke.LambdaMetafactory'
failed to load class `java.lang.invoke.MethodHandle'
failed to load class `java.lang.invoke.MethodType'
failed to load class `java.lang.invoke.MethodHandles$Lookup'
failed to load class `java.lang.invoke.CallSite'
failed to load class `java.util.Spliterators'
failed to load class `java.util.PrimitiveIterator$OfInt'
failed to load class `java.util.Spliterator$OfInt'
failed to load class `java.util.stream.StreamSupport'
failed to load class `java.util.stream.IntStream'
failed to load class `java.util.Spliterator'
failed to load class `java.util.function.Supplier'
failed to load class `java.util.NoSuchElementException'
failed to load class `java.util.function.IntConsumer'
failed to load class `java.lang.Comparable'
failed to load class `java.util.Locale'
failed to load class `java.lang.CharacterName'
failed to load class `java.lang.CharacterData'
failed to load class `java.lang.Byte'
failed to load class `java.io.UnsupportedEncodingException'
failed to load class `java.util.Comparator'
failed to load class `java.lang.Iterable'
failed to load class `java.util.Iterator'
failed to load class `java.nio.charset.Charset'
failed to load class `java.io.BufferedInputStream'
failed to load class `java.lang.Number'
failed to load class `java.lang.Long'
failed to load class `java.lang.Appendable'
failed to load class `java.util.HashMap'
failed to load class `sun.reflect.Reflection'
failed to load class `java.lang.System'
failed to load class `java.lang.SecurityManager'
failed to load class `java.lang.ClassLoader'
failed to load class `java.util.Map'
failed to load class `java.io.ObjectStreamException'
failed to load class `java.io.InvalidObjectException'
failed to load class `java.util.Arrays'
failed to load class `java.util.stream.DoubleStream'
failed to load class `java.util.stream.LongStream'
Converting
Method: java::java.lang.Object.getClass
 could not parse signature: ()Ljava/lang/Class<*>;
 Unsupported class signature: wild card generic
 reverting to descriptor: ()Ljava/lang/Class;
Method: java::java.lang.String.join
 could not parse signature: (Ljava/lang/CharSequence;Ljava/lang/Iterable<+Ljava/lang/CharSequence;>;)Ljava/lang/String;
 Unsupported class signature: wild card generic
 reverting to descriptor: (Ljava/lang/CharSequence;Ljava/lang/Iterable;)Ljava/lang/String;
Method: java::MinePumpSystem.Environment$WaterLevelEnum.<init>
 signature: ()V
 descriptor: (Ljava/lang/String;I)V
 different number of parameters, reverting to descriptor
Method: java::java.lang.Class.forName
 could not parse signature: (Ljava/lang/String;)Ljava/lang/Class<*>;
 Unsupported class signature: wild card generic
 reverting to descriptor: (Ljava/lang/String;)Ljava/lang/Class;
Method: java::java.lang.Class.forName
 could not parse signature: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class<*>;
 Unsupported class signature: wild card generic
 reverting to descriptor: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class;
Method: java::java.lang.Class.desiredAssertionStatus0
 could not parse signature: (Ljava/lang/Class<*>;)Z
 Unsupported class signature: wild card generic
 reverting to descriptor: (Ljava/lang/Class;)Z
Method: java::java.lang.Character$UnicodeScript.<init>
 signature: ()V
 descriptor: (Ljava/lang/String;I)V
 different number of parameters, reverting to descriptor
Class: java.lang.Enum
 could not parse signature: <E:Ljava/lang/Enum<TE;>;>Ljava/lang/Object;Ljava/lang/Comparable<TE;>;Ljava/io/Serializable;
 Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum<TE
 ignoring that the class is generic
Method: java::java.lang.Enum.valueOf
 could not parse signature: <T:Ljava/lang/Enum<TT;>;>(Ljava/lang/Class<TT;>;Ljava/lang/String;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;
Method: java::org.cprover.CProver.nondetWithNull
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNull
 could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
 could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNullForNotModelled
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNullForNotModelled
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Java: added 2278 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 11 object bits, 53 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1  thread 0
Unwinding loop __CPROVER__start.0 iteration 2  thread 0
Unwinding loop __CPROVER__start.0 iteration 3  thread 0
Unwinding loop __CPROVER__start.0 iteration 4  thread 0
Unwinding loop __CPROVER__start.0 iteration 5  thread 0
Unwinding recursion java::Main::clinit_wrapper iteration 1
Unwinding recursion java::Actions::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.MinePump::clinit_wrapper iteration 1
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 1 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 86 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 80 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 2 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 86 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0
aborting path on assume(false) at file MinePumpSystem/MinePump.java line 80 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 3 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 1 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2  thread 0
Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3  thread 0
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1
aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0
aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0
aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0
aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0
aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0
Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 2 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0
size of program expression: 41618 steps
simple slicing removed 1 assignments
Generated 359 VCC(s), 30 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
1834995 variables, 5674121 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime decision procedure: 22.8607s
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=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 5 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 6 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  low_constarray={ (char)'l', (char)'o', (char)'w' } ({ 00000000 01101100, 00000000 01101111, 00000000 01110111 })

State 7 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, 00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 8  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 11  thread 0
----------------------------------------------------
  this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 12  thread 0
----------------------------------------------------
  name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 13  thread 0
----------------------------------------------------
  isAnnotation=false (00000000)

State 14  thread 0
----------------------------------------------------
  isArray=false (00000000)

State 15  thread 0
----------------------------------------------------
  isInterface=false (00000000)

State 16  thread 0
----------------------------------------------------
  isSynthetic=false (00000000)

State 17  thread 0
----------------------------------------------------
  isLocalClass=false (00000000)

State 18  thread 0
----------------------------------------------------
  isMemberClass=false (00000000)

State 19  thread 0
----------------------------------------------------
  isEnum=false (00000000)

State 21 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
  MinePumpSystem.MinePump@class_model.name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 23 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 25 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 27 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 29 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 31 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 33 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 35 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 38 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  high={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=4, .data=high_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 39 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  cleanupTimeShifts=0 (00000000 00000000 00000000 00000000)

State 40 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  java$$Main$$clinit_already_run=false (0)

State 41 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 42 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 43 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  $assertionsDisabled=false (00000000)

State 45 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  java$$MinePumpSystem_MinePump$$clinit_already_run=false (0)

State 46 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  $assertionsDisabled=false (00000000)

State 47  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 50  thread 0
----------------------------------------------------
  this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 51  thread 0
----------------------------------------------------
  name=&Actions.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 52  thread 0
----------------------------------------------------
  isAnnotation=false (00000000)

State 53  thread 0
----------------------------------------------------
  isArray=false (00000000)

State 54  thread 0
----------------------------------------------------
  isInterface=false (00000000)

State 55  thread 0
----------------------------------------------------
  isSynthetic=false (00000000)

State 56  thread 0
----------------------------------------------------
  isLocalClass=false (00000000)

State 57  thread 0
----------------------------------------------------
  isMemberClass=false (00000000)

State 58  thread 0
----------------------------------------------------
  isEnum=false (00000000)

State 60 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
  Actions@class_model.name=&Actions.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 62 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 64 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 66 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 68 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 70 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 72 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 74 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 76 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  normal_return_value=0 (00000000 00000000 00000000 00000000)

State 77 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  low_return_value=0 (00000000 00000000 00000000 00000000)

State 78 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  normal={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=6, .data=normal_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 79 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 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
----------------------------------------------------
  high_constarray={ (char)'h', (char)'i', (char)'g', (char)'h' } ({ 00000000 01101000, 00000000 01101001, 00000000 01100111, 00000000 01101000 })

State 82 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 83 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  java$$Actions$$clinit_already_run=false (0)

State 84 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 85 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 97  thread 0
----------------------------------------------------
  dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 99  thread 0
----------------------------------------------------
  dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 100  thread 0
----------------------------------------------------
  dynamic_object1.length=4 (00000000 00000000 00000000 00000100)

State 103  thread 0
----------------------------------------------------
  dynamic_object1.data=dynamic_2_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 104  thread 0
----------------------------------------------------
  dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 109 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 111 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 117  thread 0
----------------------------------------------------
  dynamic_object4=dynamic_object4#1 (?)

State 121  thread 0
----------------------------------------------------
  dynamic_object4={  } ( })

State 126  thread 0
----------------------------------------------------
  dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 127 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)

State 132 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 134 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 140  thread 0
----------------------------------------------------
  dynamic_object6=dynamic_object6#1 (?)

State 144  thread 0
----------------------------------------------------
  dynamic_object6={  } ( })

State 149  thread 0
----------------------------------------------------
  dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 150 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)

State 155 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.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 157 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 (00000101 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 163  thread 0
----------------------------------------------------
  dynamic_object8=dynamic_object8#1 (?)

State 167  thread 0
----------------------------------------------------
  dynamic_object8={  } ( })

State 172  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, 00000101 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 173 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 178 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.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 180 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 (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 186  thread 0
----------------------------------------------------
  dynamic_object10=dynamic_object10#1 (?)

State 190  thread 0
----------------------------------------------------
  dynamic_object10={  } ( })

State 195  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, 00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 196 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 200 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 203 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
  arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 207  thread 0
----------------------------------------------------
  java$$Main$$clinit_already_run=true (1)

State 214 file Main.java line 8 function java::Main.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
  cleanupTimeShifts=2 (00000000 00000000 00000000 00000010)

State 219 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 220  thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 221  thread 0
----------------------------------------------------
  anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 226  thread 0
----------------------------------------------------
  java$$Actions$$clinit_already_run=true (1)

State 234 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 235  thread 0
----------------------------------------------------
  loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 240 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
  this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 241  thread 0
----------------------------------------------------
  cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 246 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
  this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 250 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 257 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 262 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
  clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 279 file Actions.java line 4 function java::Actions.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
  $assertionsDisabled=false (00000000)

State 284 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.String",
    .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 286 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 290 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 296 file Actions.java line 14 function java::Actions.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 298 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 302 file Actions.java line 10 function java::Actions.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object13.methAndRunningLastTime=false (00000000)

State 304 file Actions.java line 11 function java::Actions.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
  dynamic_object13.switchedOnBeforeTS=false (00000000)

State 305 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.String",
    .cproverMonitorCount=0 },
    .waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 })

State 307 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 311 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 11 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 315 file MinePumpSystem/Environment.java line 3 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 317 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 323  thread 0
----------------------------------------------------
  java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1)

State 335 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.String",
    .cproverMonitorCount=0 },
    .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })

State 337 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 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 341 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 4 thread 0
----------------------------------------------------
  this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 342 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 4 thread 0
----------------------------------------------------
  arg1a=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 343 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 347 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 348 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 349 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 353 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 355 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 359 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object15.@java.lang.Enum.name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 361 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 371 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 5 thread 0
----------------------------------------------------
  low=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 377 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.String",
    .cproverMonitorCount=0 },
    .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })

State 379 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 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 383 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 10 thread 0
----------------------------------------------------
  this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 384 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 10 thread 0
----------------------------------------------------
  arg1a=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 385 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 389 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 390 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 391 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 395 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 397 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 401 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object16.@java.lang.Enum.name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 403 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 413 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 11 thread 0
----------------------------------------------------
  normal=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 419 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.String",
    .cproverMonitorCount=0 },
    .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } })

State 421 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 425 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 16 thread 0
----------------------------------------------------
  this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 426 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 16 thread 0
----------------------------------------------------
  arg1a=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 427 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 431 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 432 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<init>:(Ljava/lang/String;I)V bytecode-index 3 thread 0
----------------------------------------------------
  name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 433 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 437 file java/lang/Enum.java line 117 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 439 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 443 file java/lang/Enum.java line 118 function java::java.lang.Enum.<init>:(Ljava/lang/String;I)V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object17.@java.lang.Enum.name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 445 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 455 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 17 thread 0
----------------------------------------------------
  high=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 457 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.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 459 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 460 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 463 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 19 thread 0
----------------------------------------------------
  dynamic_object18.data=dynamic_19_array (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 464 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 476 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 23 thread 0
----------------------------------------------------
  dynamic_19_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 488 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 27 thread 0
----------------------------------------------------
  dynamic_19_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 500 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 31 thread 0
----------------------------------------------------
  dynamic_19_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 506 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.<clinit>:()V bytecode-index 32 thread 0
----------------------------------------------------
  $VALUES=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 512 file MinePumpSystem/Environment.java line 11 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object14.waterLevel=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 514 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.<init>:()V bytecode-index 7 thread 0
----------------------------------------------------
  dynamic_object14.methaneLevelCritical=false (00000000)

State 518 file Actions.java line 15 function java::Actions.<init>:()V bytecode-index 12 thread 0
----------------------------------------------------
  dynamic_object13.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 522  thread 0
----------------------------------------------------
  java$$MinePumpSystem_MinePump$$clinit_already_run=true (1)

State 530 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 531  thread 0
----------------------------------------------------
  loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 536 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 537  thread 0
----------------------------------------------------
  cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 542 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 546 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 553 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 558 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 575 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
  $assertionsDisabled=false (00000000)

State 580 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.String",
    .cproverMonitorCount=0 },
    .pumpRunning=false, .systemActive=false,
    .env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 582 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 587 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 588 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 18 thread 0
----------------------------------------------------
  arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 592 file MinePumpSystem/MinePump.java line 21 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 594 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 598 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 600 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 602 file MinePumpSystem/MinePump.java line 22 function java::MinePumpSystem.MinePump.<init>:(LMinePumpSystem/Environment;)V bytecode-index 10 thread 0
----------------------------------------------------
  dynamic_object20.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 606 file Actions.java line 16 function java::Actions.<init>:()V bytecode-index 19 thread 0
----------------------------------------------------
  dynamic_object13.p=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 609 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::1a=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 610 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 612  thread 0
----------------------------------------------------
  anonlocal::6i=0 (00000000 00000000 00000000 00000000)

State 613  thread 0
----------------------------------------------------
  anonlocal::5i=0 (00000000 00000000 00000000 00000000)

State 614  thread 0
----------------------------------------------------
  anonlocal::4i=0 (00000000 00000000 00000000 00000000)

State 615  thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 619 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0
----------------------------------------------------
  anonlocal::2i=1 (00000000 00000000 00000000 00000001)

State 626  thread 0
----------------------------------------------------
  anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 629 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
  dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })

State 631 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 635 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 639 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 641 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 646 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 650 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 665 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0
----------------------------------------------------
  anonlocal::3i=1 (00000000 00000000 00000000 00000001)

State 672  thread 0
----------------------------------------------------
  anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 675 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0
----------------------------------------------------
  dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })

State 677 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 681 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 685 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 687 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 692 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 696 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 711 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0
----------------------------------------------------
  anonlocal::4i=0 (00000000 00000000 00000000 00000000)

State 718  thread 0
----------------------------------------------------
  anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 721 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.String",
    .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })

State 723 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 727 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 731 file java/util/Random.java line 116 function java::java.util.Random.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 733 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 738 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 742 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 757 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0
----------------------------------------------------
  anonlocal::5i=1 (00000000 00000000 00000000 00000001)

State 758 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0
----------------------------------------------------
  anonlocal::6i=0 (00000000 00000000 00000000 00000000)

State 765 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 770 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 775  thread 0
----------------------------------------------------
  java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1)

State 778  thread 0
----------------------------------------------------
  anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 797 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.values:()[LMinePumpSystem/Environment$WaterLevelEnum; bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 800  thread 0
----------------------------------------------------
  dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 802  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 803  thread 0
----------------------------------------------------
  dynamic_object25.length=3 (00000000 00000000 00000000 00000011)

State 806  thread 0
----------------------------------------------------
  dynamic_object25.data=dynamic_26_array (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 807  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 811  thread 0
----------------------------------------------------
  dynamic_26_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 815  thread 0
----------------------------------------------------
  dynamic_26_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 819  thread 0
----------------------------------------------------
  dynamic_26_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 839 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.String",
    .cproverMonitorCount=0 },
    .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })

State 841 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 842 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 845 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
  dynamic_object27.data=dynamic_28_array (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 846 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 852 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 11100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 867 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
  this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 879 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 895 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 13 thread 0
----------------------------------------------------
  this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 907 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 923 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.<clinit>:()V bytecode-index 20 thread 0
----------------------------------------------------
  this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 935 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 945 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0
----------------------------------------------------
  this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 966 file MinePumpSystem/Environment.java line 38 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 12 thread 0
----------------------------------------------------
  dynamic_object14.waterLevel=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 978 file Main.java line 42 function java::Main.randomSequenceOfActions:(I)V bytecode-index 33 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 984 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 999 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1005 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1015 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1021 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1028 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object13.switchedOnBeforeTS=false (00000000)

State 1036 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1044 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1054 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1064 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1065  thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1066  thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1067  thread 0
----------------------------------------------------
  anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1075 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1081 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1085 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1091 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1096 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1102 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1111 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1112  thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1113  thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1114  thread 0
----------------------------------------------------
  anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1122 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1128 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1132 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1138 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1143 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1149 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1153 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0
----------------------------------------------------
  dynamic_object13.methAndRunningLastTime=false (00000000)

State 1160 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0
----------------------------------------------------
  this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1161  thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1162  thread 0
----------------------------------------------------
  anonlocal::4i=0 (00000000 00000000 00000000 00000000)

State 1163  thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1165  thread 0
----------------------------------------------------
  anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1174 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1180 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0
----------------------------------------------------
  anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1184 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1190 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0
----------------------------------------------------
  anonlocal::2i=0 (00000000 00000000 00000000 00000000)

State 1195 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0
----------------------------------------------------
  this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1201 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0
----------------------------------------------------
  anonlocal::3i=0 (00000000 00000000 00000000 00000000)

State 1205 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0
----------------------------------------------------
  this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1219 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0
----------------------------------------------------
  anonlocal::4i=1 (00000000 00000000 00000000 00000001)

State 1230 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
  dynamic_object70={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
    .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 1232 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0
----------------------------------------------------
  dynamic_object70={ .@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 1236 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0
----------------------------------------------------
  this=&dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1240 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1244 file java/lang/Error.java line 58 function java::java.lang.Error.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1248 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
  this=&dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 1250 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
  dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)

State 1254 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
  dynamic_object70.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object70.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001100 10000000 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