./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product38_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.XNVj9X.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product38_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_product38_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 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 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 104 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 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 104 function java::MinePumpSystem.MinePump.startSystem:()V bytecode-index 8 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: 46723 steps simple slicing removed 1 assignments Generated 391 VCC(s), 27 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 1913467 variables, 5772859 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 22.0901s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 5 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 8 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 9 thread 0 ---------------------------------------------------- name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 10 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 11 thread 0 ---------------------------------------------------- isArray=false (00000000) State 12 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 13 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 14 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 15 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 16 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 18 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 (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 20 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 22 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 24 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 26 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 28 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 30 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 32 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 35 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 36 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 37 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- cleanupTimeShifts=0 (00000000 00000000 00000000 00000000) State 38 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 39 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 41 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 42 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=false (0) State 43 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 44 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=3, .data=low_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 45 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_return_value=0 (00000000 00000000 00000000 00000000) State 46 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 47 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 48 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 49 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal_return_value=0 (00000000 00000000 00000000 00000000) State 50 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 51 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high_return_value=0 (00000000 00000000 00000000 00000000) State 52 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 53 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 54 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=false (0) State 55 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 58 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 59 thread 0 ---------------------------------------------------- name=&Actions.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 60 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 61 thread 0 ---------------------------------------------------- isArray=false (00000000) State 62 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 63 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 64 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 65 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 66 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 68 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 70 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 72 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 74 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 76 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 78 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 80 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 82 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 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=false (0) State 85 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$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=2 (00000000 00000000 00000000 00000010) State 103 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000100 10100000 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 (00000100 11000000 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, 00000100 11100000 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 00000000 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 150 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 154 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 157 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 161 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 168 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- cleanupTimeShifts=2 (00000000 00000000 00000000 00000010) State 173 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V bytecode-index 1 thread 0 ---------------------------------------------------- arg0i=3 (00000000 00000000 00000000 00000011) State 174 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 175 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 180 thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=true (1) State 188 file Actions.java line 4 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 189 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 194 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 195 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 200 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 204 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 211 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 216 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 233 file Actions.java line 4 function java::Actions.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 238 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .env=null, .p=null, .methAndRunningLastTime=false, .switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 }) State 240 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::Actions", .cproverMonitorCount=0 }, .env=null, .p=null, .methAndRunningLastTime=false, .switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 }) State 244 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 250 file Actions.java line 14 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 252 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 256 file Actions.java line 10 function java::Actions.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 258 file Actions.java line 11 function java::Actions.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 259 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 261 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 265 file Actions.java line 15 function java::Actions.:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 269 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 271 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 277 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1) State 289 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 291 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 295 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 296 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 297 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg2i=0 (00000000 00000000 00000000 00000000) State 301 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 302 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 303 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 307 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 (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 309 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 313 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 315 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 325 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 (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 331 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 333 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 337 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 338 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 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 339 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg2i=1 (00000000 00000000 00000000 00000001) State 343 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 344 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- name=&normal.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 345 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 349 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 351 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 355 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 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 357 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 367 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 373 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 375 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 379 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 380 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg1a=&high.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 381 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg2i=2 (00000000 00000000 00000000 00000010) State 385 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 386 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- name=&high.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 387 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 391 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 393 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 397 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 (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 399 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 409 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 411 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 413 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 414 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 417 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.data=dynamic_19_array (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 418 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 430 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 (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 442 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 454 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 460 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 466 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 468 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 472 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 476 thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=true (1) State 484 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 485 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 490 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 491 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 496 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 500 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 507 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 512 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 529 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 534 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 536 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 541 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 542 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 546 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 548 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 552 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=false (00000000) State 554 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 556 file MinePumpSystem/MinePump.java line 22 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 10 thread 0 ---------------------------------------------------- dynamic_object20.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 560 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 563 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 564 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 566 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 567 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 568 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 569 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 573 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 580 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 583 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 585 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 589 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 593 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 595 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 600 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 604 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 619 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 626 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 629 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 631 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 635 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 639 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 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 641 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 646 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 650 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 665 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 672 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 675 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 677 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 681 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 685 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 (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 687 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 692 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 696 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 711 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 712 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 721 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 724 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 726 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 730 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 734 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 (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 736 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 741 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object24.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 745 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 760 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 772 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 778 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 788 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 794 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 801 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 809 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 817 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 823 file MinePumpSystem/MinePump.java line 56 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 830 file MinePumpSystem/MinePump.java line 43 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 837 file MinePumpSystem/MinePump.java line 99 function java::MinePumpSystem.MinePump.isHighWaterLevel:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 864 file MinePumpSystem/MinePump.java line 47 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 880 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 890 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 891 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 892 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 893 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 901 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 907 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 911 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 917 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 922 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 928 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 937 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 938 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 939 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 940 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 948 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 954 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 958 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 964 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 969 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 975 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 979 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 986 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 987 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 988 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 989 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 991 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1000 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1006 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1010 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1016 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1021 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1027 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1031 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1045 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1055 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1056 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1058 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1066 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1072 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1077 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1083 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1087 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1101 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1102 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1111 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1112 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1114 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1122 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1128 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1133 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1139 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1143 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1157 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1158 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1170 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1171 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1172 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1173 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1177 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=2 (00000000 00000000 00000000 00000010) State 1184 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1187 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object57={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1189 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object57={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1193 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object57.@java.lang.Object.@class_identifier (00001010 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1197 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object57.@java.lang.Object.@class_identifier (00001010 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1199 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object57.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1204 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object57.@java.lang.Object.@class_identifier (00001010 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1208 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object57.@java.lang.Object.@class_identifier (00001010 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1223 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1230 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1233 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object58={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1235 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object58={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1239 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object58.@java.lang.Object.@class_identifier (00001011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1243 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object58.@java.lang.Object.@class_identifier (00001011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1245 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object58.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1250 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object58.@java.lang.Object.@class_identifier (00001011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1254 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object58.@java.lang.Object.@class_identifier (00001011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1269 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1276 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1279 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object59={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1281 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object59={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1285 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object59.@java.lang.Object.@class_identifier (00001011 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1289 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object59.@java.lang.Object.@class_identifier (00001011 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1291 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object59.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1296 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object59.@java.lang.Object.@class_identifier (00001011 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1300 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object59.@java.lang.Object.@class_identifier (00001011 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1315 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=1 (00000000 00000000 00000000 00000001) State 1316 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1327 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1333 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1348 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1354 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1364 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1370 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1377 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 1385 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1393 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1399 file MinePumpSystem/MinePump.java line 56 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1406 file MinePumpSystem/MinePump.java line 43 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1413 file MinePumpSystem/MinePump.java line 99 function java::MinePumpSystem.MinePump.isHighWaterLevel:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1440 file MinePumpSystem/MinePump.java line 47 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1456 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1466 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1467 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1468 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1469 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1477 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1483 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1487 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1493 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1498 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1504 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1513 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1514 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1515 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1516 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1524 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1530 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1534 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1540 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1545 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1551 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1555 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 1562 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1563 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1564 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1565 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1567 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1576 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1582 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1586 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1592 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1597 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1603 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1607 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1621 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1631 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1632 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1634 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1642 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1648 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1653 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1659 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1663 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1677 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1678 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1687 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1688 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1690 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1698 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1704 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1709 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1715 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1719 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1733 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1734 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1746 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1747 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1748 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1749 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1753 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=3 (00000000 00000000 00000000 00000011) State 1760 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1763 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object172={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1765 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object172={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1769 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object172.@java.lang.Object.@class_identifier (00011000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1773 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object172.@java.lang.Object.@class_identifier (00011000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1775 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object172.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1780 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object172.@java.lang.Object.@class_identifier (00011000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1784 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object172.@java.lang.Object.@class_identifier (00011000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1799 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1806 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1809 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object173={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1811 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object173={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1815 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object173.@java.lang.Object.@class_identifier (00011000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1819 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object173.@java.lang.Object.@class_identifier (00011000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1821 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object173.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1826 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object173.@java.lang.Object.@class_identifier (00011000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1830 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object173.@java.lang.Object.@class_identifier (00011000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1845 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1852 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1855 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object174={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1857 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object174={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1861 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object174.@java.lang.Object.@class_identifier (00011000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1865 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object174.@java.lang.Object.@class_identifier (00011000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1867 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object174.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1872 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object174.@java.lang.Object.@class_identifier (00011000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1876 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object174.@java.lang.Object.@class_identifier (00011000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1891 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=1 (00000000 00000000 00000000 00000001) State 1892 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1899 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1904 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1909 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1) State 1912 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1931 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1934 thread 0 ---------------------------------------------------- dynamic_object177={ .@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 1936 thread 0 ---------------------------------------------------- dynamic_object177={ .@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 1937 thread 0 ---------------------------------------------------- dynamic_object177.length=3 (00000000 00000000 00000000 00000011) State 1940 thread 0 ---------------------------------------------------- dynamic_object177.data=dynamic_178_array (00011001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1941 thread 0 ---------------------------------------------------- dynamic_178_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 1945 thread 0 ---------------------------------------------------- dynamic_178_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1949 thread 0 ---------------------------------------------------- dynamic_178_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1953 thread 0 ---------------------------------------------------- dynamic_178_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1973 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object181={ .@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 1975 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object181={ .@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 1976 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object181.length=3 (00000000 00000000 00000000 00000011) State 1979 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object181.data=dynamic_182_array (00000010 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1980 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_182_array={ 0, 0, 0 } ({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 }) State 1986 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 3 thread 0 ---------------------------------------------------- $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=&dynamic_object181.@java.lang.Object.@class_identifier (00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2001 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 2013 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 8 thread 0 ---------------------------------------------------- dynamic_182_array[2L]=1 (00000000 00000000 00000000 00000001) State 2029 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 2041 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 15 thread 0 ---------------------------------------------------- dynamic_182_array[1L]=2 (00000000 00000000 00000000 00000010) State 2057 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 (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2069 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_182_array[0L]=3 (00000000 00000000 00000000 00000011) State 2079 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 2100 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 2112 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2118 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2133 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 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2139 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2149 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2155 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2162 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 2170 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2178 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2184 file MinePumpSystem/MinePump.java line 56 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2191 file MinePumpSystem/MinePump.java line 43 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2198 file MinePumpSystem/MinePump.java line 99 function java::MinePumpSystem.MinePump.isHighWaterLevel:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2223 file MinePumpSystem/MinePump.java line 44 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 7 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2225 file MinePumpSystem/MinePump.java line 63 function java::MinePumpSystem.MinePump.activatePump:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=true (00000001) State 2231 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2248 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2258 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2259 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2260 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2261 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2269 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2275 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2279 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2285 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2290 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2296 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2305 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2306 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2307 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2308 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2316 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2322 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2326 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2332 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2337 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2343 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2347 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 2354 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2355 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2356 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 2357 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2359 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2368 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2374 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2378 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2384 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2389 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2395 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2399 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2413 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 2424 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2425 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2427 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2435 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2441 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2446 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2452 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 2456 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2470 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2471 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2480 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2481 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2483 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2491 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2497 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2502 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2508 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 2512 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2526 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2527 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2538 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 43 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2547 file Main.java line 51 function java::Main.randomSequenceOfActions:(I)V bytecode-index 48 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2553 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2563 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2569 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2576 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=true (00000001) State 2584 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2591 file MinePumpSystem/MinePump.java line 29 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2602 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment.lowerWaterLevel:()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 2623 file MinePumpSystem/Environment.java line 22 function java::MinePumpSystem.Environment.lowerWaterLevel:()V bytecode-index 8 thread 0 ---------------------------------------------------- dynamic_object14.waterLevel=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2633 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2640 file MinePumpSystem/MinePump.java line 53 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2646 file MinePumpSystem/MinePump.java line 80 function java::MinePumpSystem.MinePump.isMethaneAlarm:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2661 file MinePumpSystem/MinePump.java line 56 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2667 file MinePumpSystem/MinePump.java line 47 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2683 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2693 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2694 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2695 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2696 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2704 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2710 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2714 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2720 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2725 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2731 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2740 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2741 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2742 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2743 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2751 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2757 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2761 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2767 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2772 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2778 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2782 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 2789 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2790 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2791 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 2792 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2794 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2803 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2809 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2813 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2819 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2824 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2830 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2834 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2848 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 2858 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2859 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2861 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2869 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2875 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2880 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2886 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 2890 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2904 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2905 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2914 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2915 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 2917 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2925 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2931 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2936 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2942 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 2946 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 2960 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 2961 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 2972 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 49 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 2982 file Main.java line 51 function java::Main.randomSequenceOfActions:(I)V bytecode-index 48 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2988 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 2998 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3004 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3011 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=true (00000001) State 3019 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3026 file MinePumpSystem/MinePump.java line 29 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3037 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment.lowerWaterLevel:()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 3059 file MinePumpSystem/Environment.java line 25 function java::MinePumpSystem.Environment.lowerWaterLevel:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object14.waterLevel=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3068 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3075 file MinePumpSystem/MinePump.java line 53 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3081 file MinePumpSystem/MinePump.java line 80 function java::MinePumpSystem.MinePump.isMethaneAlarm:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3096 file MinePumpSystem/MinePump.java line 56 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3102 file MinePumpSystem/MinePump.java line 47 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__highWaterSensor:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3118 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3128 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3129 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 3130 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3131 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3139 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3145 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3149 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3155 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3160 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3166 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 3175 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3176 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 3177 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3178 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3186 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3192 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3196 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3202 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3207 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3213 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 3217 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 3224 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3225 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 3226 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 3227 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3229 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3238 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3244 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3248 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3254 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3259 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3265 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 3269 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3283 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 3293 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3294 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 3296 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3304 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3310 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3315 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 3321 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 3325 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3339 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 3340 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 3350 file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_object443={ .@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 3352 file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_object443={ .@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 3356 file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 24 thread 0 ---------------------------------------------------- this=&dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00111000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3360 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00111000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3364 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00111000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3368 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00111000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 3370 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 3374 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object443.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object443.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00111000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 assertion at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 false VERIFICATION FAILED EC=10 FALSE