./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product32_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.ig0Tg5.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product32_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_product32_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 120 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 114 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 120 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 thread 0 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 114 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: 49705 steps simple slicing removed 1 assignments Generated 439 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 2116854 variables, 6694046 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 29.0033s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 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 7 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 8 thread 0 ---------------------------------------------------- name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 9 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 10 thread 0 ---------------------------------------------------- isArray=false (00000000) State 11 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 12 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 13 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 14 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 15 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 17 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 19 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 21 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 23 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 25 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 27 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 29 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 31 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 34 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 35 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 36 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 37 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 38 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_return_value=0 (00000000 00000000 00000000 00000000) State 39 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 40 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 41 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=false (0) State 42 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 44 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 45 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 46 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- cleanupTimeShifts=0 (00000000 00000000 00000000 00000000) State 47 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=false (0) State 48 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 49 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 50 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 51 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 52 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal_return_value=0 (00000000 00000000 00000000 00000000) State 53 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 54 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 55 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high_return_value=0 (00000000 00000000 00000000 00000000) State 56 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 59 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 60 thread 0 ---------------------------------------------------- name=&Actions.@java.lang.Object.@class_identifier (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 61 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 62 thread 0 ---------------------------------------------------- isArray=false (00000000) State 63 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 64 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 65 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 66 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 67 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 69 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 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 71 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 73 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 75 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 77 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 79 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 81 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 83 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 85 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 97 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 99 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 100 thread 0 ---------------------------------------------------- dynamic_object1.length=3 (00000000 00000000 00000000 00000011) State 103 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 104 thread 0 ---------------------------------------------------- dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 109 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 111 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 117 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 121 thread 0 ---------------------------------------------------- dynamic_object4={ } ( }) State 126 thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 127 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 132 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 134 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 140 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 144 thread 0 ---------------------------------------------------- dynamic_object6={ } ( }) State 149 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 150 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 155 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 157 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[2L]=&dynamic_object7.@java.lang.Object.@class_identifier (00000101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 163 thread 0 ---------------------------------------------------- dynamic_object8=dynamic_object8#1 (?) State 167 thread 0 ---------------------------------------------------- dynamic_object8={ } ( }) State 172 thread 0 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 173 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object7.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 177 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 180 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 184 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 191 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- cleanupTimeShifts=2 (00000000 00000000 00000000 00000010) State 196 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 197 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 198 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 203 thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=true (1) State 211 file Actions.java line 4 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 212 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 217 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 218 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 223 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 227 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 234 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 239 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 256 file Actions.java line 4 function java::Actions.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 261 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 263 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 267 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 273 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 275 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 279 file Actions.java line 10 function java::Actions.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 281 file Actions.java line 11 function java::Actions.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 282 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 284 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 288 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 292 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 294 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 300 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1) State 312 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 314 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 318 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 319 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 320 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg2i=0 (00000000 00000000 00000000 00000000) State 324 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 325 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 326 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 330 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 332 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 336 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 338 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 348 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 354 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 356 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 360 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 361 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 362 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg2i=1 (00000000 00000000 00000000 00000001) State 366 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 367 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 368 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 372 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 374 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 378 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 380 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 390 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 396 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 398 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 402 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 403 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 404 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg2i=2 (00000000 00000000 00000000 00000010) State 408 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 409 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 410 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 414 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 416 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 420 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 422 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 432 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 434 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 436 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 437 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 440 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 441 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 453 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 465 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 477 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 483 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 489 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 491 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 495 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 499 thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=true (1) State 507 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 508 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 513 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 514 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 519 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 523 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 530 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 535 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 552 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 557 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 559 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 564 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 565 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 569 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 571 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 575 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=false (00000000) State 577 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 579 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 583 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 586 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 587 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 589 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 590 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 591 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 592 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 596 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 603 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 606 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 608 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 612 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 616 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 618 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 623 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 627 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 642 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 649 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 652 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 654 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 658 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 662 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 664 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 669 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 673 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 688 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 695 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 698 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 700 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 704 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 708 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 710 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 715 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 719 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 734 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 735 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 744 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 747 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 749 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 753 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 757 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 759 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 764 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 768 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 783 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=1 (00000000 00000000 00000000 00000001) State 788 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 793 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 798 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1) State 801 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 820 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 823 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 825 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 826 thread 0 ---------------------------------------------------- dynamic_object25.length=3 (00000000 00000000 00000000 00000011) State 829 thread 0 ---------------------------------------------------- dynamic_object25.data=dynamic_26_array (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 830 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 834 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 838 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 842 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 862 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 864 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 865 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 868 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 869 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 875 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 890 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 902 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 918 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 930 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 946 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 958 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 968 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 989 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 999 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 1004 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 1013 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=true (00000001) State 1024 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 1030 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 1041 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 1053 file MinePumpSystem/MinePump.java line 115 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 16 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=false (00000000) State 1062 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 1068 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 1081 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 1093 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 1106 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1107 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1108 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1109 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1113 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=2 (00000000 00000000 00000000 00000010) State 1120 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1123 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object101={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1125 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object101={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1129 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object101.@java.lang.Object.@class_identifier (00010000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1133 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object101.@java.lang.Object.@class_identifier (00010000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1135 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object101.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1140 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object101.@java.lang.Object.@class_identifier (00010000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1144 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object101.@java.lang.Object.@class_identifier (00010000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1159 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1166 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1169 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object102={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1171 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object102={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1175 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object102.@java.lang.Object.@class_identifier (00010000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1179 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object102.@java.lang.Object.@class_identifier (00010000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1181 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object102.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1186 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object102.@java.lang.Object.@class_identifier (00010000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1190 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object102.@java.lang.Object.@class_identifier (00010000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1205 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1212 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1215 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object103={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1217 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object103={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1221 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object103.@java.lang.Object.@class_identifier (00010000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1225 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object103.@java.lang.Object.@class_identifier (00010000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1227 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object103.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1232 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object103.@java.lang.Object.@class_identifier (00010000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1236 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object103.@java.lang.Object.@class_identifier (00010000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1251 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=1 (00000000 00000000 00000000 00000001) State 1252 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1261 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 1266 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 1274 file MinePumpSystem/Environment.java line 46 function java::MinePumpSystem.Environment.changeMethaneLevel:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 1283 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 1289 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 1300 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 1310 file MinePumpSystem/MinePump.java line 121 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 11 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 1320 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 1326 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 1336 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 1342 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 1349 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 1357 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 1365 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 1371 file MinePumpSystem/MinePump.java line 54 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 1377 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__methaneQuery:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1393 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 1403 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 1404 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1405 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1406 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1414 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 1420 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 1424 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 1430 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1435 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 1441 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1450 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 1451 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1452 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1453 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1461 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 1467 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 1471 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 1477 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1482 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 1488 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1492 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 1499 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 1500 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1501 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1502 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1504 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1513 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 1519 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 1523 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 1529 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1534 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 1540 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1544 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 1558 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1569 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object206={ .@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 1571 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object206={ .@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 1575 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1579 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1583 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1587 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00011100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1589 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1593 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object206.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object206.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00011100 11000000 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