./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product28_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.Ig3bPK.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product28_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_product28_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. 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. signature: ()V descriptor: (Ljava/lang/String;I)V different number of parameters, reverting to descriptor Class: java.lang.Enum could not parse signature: ;>Ljava/lang/Object;Ljava/lang/Comparable;Ljava/io/Serializable; Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum;>(Ljava/lang/Class;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: ()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: (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: ()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: (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: ()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: ()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 111 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 105 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 2 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 111 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 105 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 3 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 1 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 2 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 size of program expression: 45511 steps simple slicing removed 1 assignments Generated 399 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 1982982 variables, 6243595 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 24.8228s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 5 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 6 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 7 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal_return_value=0 (00000000 00000000 00000000 00000000) State 8 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 9 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 10 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 12 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 15 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 16 thread 0 ---------------------------------------------------- name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 17 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 18 thread 0 ---------------------------------------------------- isArray=false (00000000) State 19 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 20 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 21 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 22 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 23 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 25 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 27 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 29 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 31 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 33 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 35 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 37 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 39 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 41 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 44 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 45 thread 0 ---------------------------------------------------- name=&Actions.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 46 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 47 thread 0 ---------------------------------------------------- isArray=false (00000000) State 48 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 49 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 50 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 51 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 52 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 54 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- Actions@class_model.name=&Actions.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 56 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 58 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 60 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 62 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 64 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 66 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 68 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 70 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high_return_value=0 (00000000 00000000 00000000 00000000) State 71 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 72 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 73 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 74 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=3, .data=low_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 75 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_return_value=0 (00000000 00000000 00000000 00000000) State 76 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 77 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=6, .data=normal_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 78 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 79 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=4, .data=high_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 80 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 81 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- cleanupTimeShifts=0 (00000000 00000000 00000000 00000000) State 82 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=false (0) State 83 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=false (0) State 96 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 98 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 99 thread 0 ---------------------------------------------------- dynamic_object1.length=0 (00000000 00000000 00000000 00000000) State 102 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 103 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 107 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 110 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 114 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 121 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- cleanupTimeShifts=2 (00000000 00000000 00000000 00000010) State 126 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 127 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 128 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 133 thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=true (1) State 141 file Actions.java line 4 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 142 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 147 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 148 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 153 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 157 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 164 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 169 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 186 file Actions.java line 4 function java::Actions.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 191 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .env=null, .p=null, .methAndRunningLastTime=false, .switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 }) State 193 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 197 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 203 file Actions.java line 14 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 205 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object13.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 209 file Actions.java line 10 function java::Actions.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 211 file Actions.java line 11 function java::Actions.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 212 file Actions.java line 15 function java::Actions.:()V bytecode-index 9 thread 0 ---------------------------------------------------- dynamic_object14={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 }) State 214 file Actions.java line 15 function java::Actions.:()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 218 file Actions.java line 15 function java::Actions.:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 222 file MinePumpSystem/Environment.java line 3 function java::MinePumpSystem.Environment.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 224 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object14.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 230 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1) State 242 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 244 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 248 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 249 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg1a=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 250 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg2i=0 (00000000 00000000 00000000 00000000) State 254 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 255 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 256 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=0 (00000000 00000000 00000000 00000000) State 260 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(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 262 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object15.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 266 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(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 268 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object15.@java.lang.Enum.ordinal=0 (00000000 00000000 00000000 00000000) State 278 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 284 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 6 thread 0 ---------------------------------------------------- dynamic_object16={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 286 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 290 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 291 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg1a=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 292 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg2i=1 (00000000 00000000 00000000 00000001) State 296 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 297 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 298 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=1 (00000000 00000000 00000000 00000001) State 302 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(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 304 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object16.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 308 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(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 310 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object16.@java.lang.Enum.ordinal=1 (00000000 00000000 00000000 00000001) State 320 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 326 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object17={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 328 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 332 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 333 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg1a=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 334 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg2i=2 (00000000 00000000 00000000 00000010) State 338 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 339 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(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 340 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=2 (00000000 00000000 00000000 00000010) State 344 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(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 346 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object17.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 350 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(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 352 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object17.@java.lang.Enum.ordinal=2 (00000000 00000000 00000000 00000010) State 362 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 364 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 366 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 367 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.length=3 (00000000 00000000 00000000 00000011) State 370 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.data=dynamic_19_array (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 371 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 383 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 395 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 407 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()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 413 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 32 thread 0 ---------------------------------------------------- $VALUES=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 419 file MinePumpSystem/Environment.java line 11 function java::MinePumpSystem.Environment.:()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 421 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 425 file Actions.java line 15 function java::Actions.:()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 429 thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=true (1) State 437 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 438 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 443 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 444 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 449 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 453 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 460 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 465 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 482 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 487 file Actions.java line 16 function java::Actions.:()V bytecode-index 14 thread 0 ---------------------------------------------------- dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .pumpRunning=false, .systemActive=false, .env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 489 file Actions.java line 16 function java::Actions.:()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 494 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 495 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 499 file MinePumpSystem/MinePump.java line 21 function java::MinePumpSystem.MinePump.:(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 501 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 505 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=false (00000000) State 507 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 509 file MinePumpSystem/MinePump.java line 22 function java::MinePumpSystem.MinePump.:(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 513 file Actions.java line 16 function java::Actions.:()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 516 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 517 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 519 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 520 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 521 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 522 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 526 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 533 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 536 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 538 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 542 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 546 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 548 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object21.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 553 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 557 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 572 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 579 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 582 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 584 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 588 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 592 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 594 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object22.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 599 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 603 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 618 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 625 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 628 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 630 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 634 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 638 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 640 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object23.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 645 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 649 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 664 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 665 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 674 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 677 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 679 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 683 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 687 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 689 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object24.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 694 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 698 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 713 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=1 (00000000 00000000 00000000 00000001) State 718 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 723 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 728 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1) State 731 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 750 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 753 thread 0 ---------------------------------------------------- dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 755 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 756 thread 0 ---------------------------------------------------- dynamic_object25.length=3 (00000000 00000000 00000000 00000011) State 759 thread 0 ---------------------------------------------------- dynamic_object25.data=dynamic_26_array (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 760 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 764 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 768 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 772 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 792 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 794 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 795 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27.length=3 (00000000 00000000 00000000 00000011) State 798 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27.data=dynamic_28_array (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 799 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 805 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 820 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 832 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 8 thread 0 ---------------------------------------------------- dynamic_28_array[2L]=1 (00000000 00000000 00000000 00000001) State 848 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 860 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 15 thread 0 ---------------------------------------------------- dynamic_28_array[1L]=2 (00000000 00000000 00000000 00000010) State 876 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()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 888 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_28_array[0L]=3 (00000000 00000000 00000000 00000011) State 898 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 919 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 933 file Main.java line 44 function java::Main.randomSequenceOfActions:(I)V bytecode-index 38 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 939 file Actions.java line 32 function java::Actions.stopSystem:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 950 file Actions.java line 33 function java::Actions.stopSystem:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 962 file MinePumpSystem/MinePump.java line 106 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 16 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=false (00000000) State 971 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 977 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 990 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 1002 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 1015 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1016 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1017 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1018 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1022 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=2 (00000000 00000000 00000000 00000010) State 1029 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1032 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object93={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1034 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object93={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1038 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1042 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1044 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object93.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1049 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1053 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object93.@java.lang.Object.@class_identifier (00001111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1068 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1075 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1078 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object94={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1080 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object94={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1084 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1088 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1090 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object94.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1095 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1099 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object94.@java.lang.Object.@class_identifier (00001111 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1114 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1121 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1124 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object95={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1126 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object95={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1130 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1134 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1136 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object95.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1141 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1145 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object95.@java.lang.Object.@class_identifier (00001111 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1160 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1161 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1170 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1173 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object96={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1175 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object96={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1179 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1183 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1185 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object96.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1190 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1194 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object96.@java.lang.Object.@class_identifier (00001111 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1209 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1216 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1221 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1230 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=true (00000001) State 1242 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 1248 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 1261 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 1273 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 1286 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1287 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1288 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1289 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1293 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=3 (00000000 00000000 00000000 00000011) State 1300 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1303 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object205={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1305 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object205={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1309 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1313 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1315 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object205.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1320 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1324 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object205.@java.lang.Object.@class_identifier (00011100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1339 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1346 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1349 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object206={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1351 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object206={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1355 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1359 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1361 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object206.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1366 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object206.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1370 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1385 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1392 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1395 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object207={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1397 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object207={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1401 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object207.@java.lang.Object.@class_identifier (00011100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1405 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object207.@java.lang.Object.@class_identifier (00011100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1407 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object207.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1412 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object207.@java.lang.Object.@class_identifier (00011100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1416 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object207.@java.lang.Object.@class_identifier (00011100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1431 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=1 (00000000 00000000 00000000 00000001) State 1432 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1439 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 1444 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 1455 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1481 file Main.java line 38 function java::Main.randomSequenceOfActions:(I)V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1486 file Actions.java line 27 function java::Actions.methaneChange:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1494 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 1503 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 1509 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 1520 file Actions.java line 39 function java::Actions.startSystem:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1530 file MinePumpSystem/MinePump.java line 112 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 11 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 1540 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 1546 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 1556 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 1562 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 1569 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 1577 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 1585 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 1591 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1604 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 1614 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 1615 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1616 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1617 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1625 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 1631 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 1635 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 1641 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1646 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 1652 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1661 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 1662 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1663 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1664 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1672 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 1678 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 1682 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 1688 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1693 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 1699 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1703 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 1710 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 1711 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1712 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1713 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1715 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1724 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 1730 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 1734 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 1740 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1745 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 1751 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1755 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 1769 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1780 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object302={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } }) State 1782 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object302={ .@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 1786 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00101000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1790 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00101000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1794 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00101000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1798 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00101000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1800 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1804 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object302.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object302.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00101000 00000000 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