./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product22_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.uXvHGo.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product22_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_product22_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 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 1 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 2 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 3 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 1 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 2 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 size of program expression: 10166 steps simple slicing removed 1 assignments Generated 19 VCC(s), 6 remaining after simplification Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier converting SSA Running string refinement loop with MiniSAT 2.2.1 without simplifier BV-Refinement: post-processing BV-Refinement: iteration 1 235947 variables, 512171 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 0.538724s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 5 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 6 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 7 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal_return_value=0 (00000000 00000000 00000000 00000000) State 8 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high_return_value=0 (00000000 00000000 00000000 00000000) State 9 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 10 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 11 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 12 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 14 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 17 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 18 thread 0 ---------------------------------------------------- name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 19 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 20 thread 0 ---------------------------------------------------- isArray=false (00000000) State 21 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 22 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 23 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 24 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 25 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 27 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 29 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 31 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 33 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 35 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 37 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 39 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 41 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 43 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=false (0) State 44 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 47 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 48 thread 0 ---------------------------------------------------- name=&Actions.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 49 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 50 thread 0 ---------------------------------------------------- isArray=false (00000000) State 51 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 52 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 53 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 54 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 55 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 57 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- Actions@class_model.name=&Actions.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 59 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 61 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 63 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 65 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 67 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 69 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 71 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 73 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 74 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 75 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $VALUES=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 76 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, 00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 77 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_return_value=0 (00000000 00000000 00000000 00000000) State 78 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 79 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, 00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 80 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 81 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=4, .data=high_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 82 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 83 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- cleanupTimeShifts=0 (00000000 00000000 00000000 00000000) State 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=false (0) State 96 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 98 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 99 thread 0 ---------------------------------------------------- dynamic_object1.length=4 (00000000 00000000 00000000 00000100) State 102 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000010 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 103 thread 0 ---------------------------------------------------- dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 108 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 110 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000010 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 116 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 120 thread 0 ---------------------------------------------------- dynamic_object4={ } ( }) State 125 thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000010 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 126 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 131 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 133 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000010 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 139 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 143 thread 0 ---------------------------------------------------- dynamic_object6={ } ( }) State 148 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000010 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 149 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 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 156 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[2L]=&dynamic_object7.@java.lang.Object.@class_identifier (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 162 thread 0 ---------------------------------------------------- dynamic_object8=dynamic_object8#1 (?) State 166 thread 0 ---------------------------------------------------- dynamic_object8={ } ( }) State 171 thread 0 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000011 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 172 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object7.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 177 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 179 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[3L]=&dynamic_object9.@java.lang.Object.@class_identifier (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 185 thread 0 ---------------------------------------------------- dynamic_object10=dynamic_object10#1 (?) State 189 thread 0 ---------------------------------------------------- dynamic_object10={ } ( }) State 194 thread 0 ---------------------------------------------------- dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object10 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000011 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 195 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object9.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 199 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 202 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 206 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 213 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- cleanupTimeShifts=2 (00000000 00000000 00000000 00000010) State 218 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 219 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 220 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 225 thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=true (1) State 233 file Actions.java line 4 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 234 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 239 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 240 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 245 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 249 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 256 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 261 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 278 file Actions.java line 4 function java::Actions.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 283 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 285 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::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 289 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 295 file Actions.java line 14 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 297 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 301 file Actions.java line 10 function java::Actions.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 303 file Actions.java line 11 function java::Actions.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 304 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 306 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 310 file Actions.java line 15 function java::Actions.:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 314 file MinePumpSystem/Environment.java line 3 function java::MinePumpSystem.Environment.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 316 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 322 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1) State 334 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 336 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 340 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 341 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg1a=&low.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 342 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg2i=0 (00000000 00000000 00000000 00000000) State 346 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 347 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 348 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 352 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 354 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 358 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 (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 360 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 370 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 376 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 378 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 382 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 383 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg1a=&normal.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 384 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg2i=1 (00000000 00000000 00000000 00000001) State 388 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 389 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 (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 390 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 394 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 396 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 400 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 (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 402 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 412 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 418 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 420 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 424 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 425 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg1a=&high.@java.lang.Object.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 426 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg2i=2 (00000000 00000000 00000000 00000010) State 430 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 431 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 (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 432 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 436 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 438 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 442 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 (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 444 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 454 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 456 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 458 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 459 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 462 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.data=dynamic_19_array (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 463 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 475 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 487 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 499 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 505 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 (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 511 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 513 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 517 file Actions.java line 15 function java::Actions.:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object13.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 521 thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=true (1) State 529 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 (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 530 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 535 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 536 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 541 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 545 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 552 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 557 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 574 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 579 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 581 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 586 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 587 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 591 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 (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 593 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 597 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=false (00000000) State 599 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 601 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 (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 605 file Actions.java line 16 function java::Actions.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object13.p=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 608 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 609 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 611 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 612 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 613 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 614 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 618 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 625 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 628 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 630 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 634 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 638 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 640 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object21.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 645 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 649 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 664 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 671 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 674 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 676 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 680 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 684 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 (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 686 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 691 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 695 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 710 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 717 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 720 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 722 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 726 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 730 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 (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 732 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 737 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 741 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 756 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=1 (00000000 00000000 00000000 00000001) State 757 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 768 file Main.java line 42 function java::Main.randomSequenceOfActions:(I)V bytecode-index 33 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 774 file Actions.java line 38 function java::Actions.startSystem:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 789 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 795 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 805 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 811 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 818 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 826 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 834 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 840 file MinePumpSystem/MinePump.java line 54 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 846 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__lowWaterSensor:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 862 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 872 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 873 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 874 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 875 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 883 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 889 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 893 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 899 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 904 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 910 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 919 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 920 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 921 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 922 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 930 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 936 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 940 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 946 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 951 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 957 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 961 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 968 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 969 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 970 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 971 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 973 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 982 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 988 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 992 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 998 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1003 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1009 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1013 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1027 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1037 file Actions.java line 53 function java::Actions.timeShift:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1038 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1040 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1048 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1054 file Actions.java line 113 function java::Actions.Specification4:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1059 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1065 file Actions.java line 115 function java::Actions.Specification4:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1069 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1083 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1084 file Actions.java line 116 function java::Actions.Specification4:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1093 file Actions.java line 54 function java::Actions.timeShift:()V bytecode-index 22 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1094 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1096 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1104 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1110 file Actions.java line 136 function java::Actions.Specification5_2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1115 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1121 file Actions.java line 138 function java::Actions.Specification5_2:()V bytecode-index 7 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1125 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1139 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1140 file Actions.java line 139 function java::Actions.Specification5_2:()V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1152 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1153 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1154 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1155 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1159 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=2 (00000000 00000000 00000000 00000010) State 1166 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1169 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object30={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1171 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object30={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1175 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1179 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1181 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object30.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1186 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1190 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object30.@java.lang.Object.@class_identifier (00000101 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1205 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 1212 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1215 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object31={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1217 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object31={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1221 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1225 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1227 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object31.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1232 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1236 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object31.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1251 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1258 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1261 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1263 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1267 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1271 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1273 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object32.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1278 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1282 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object32.@java.lang.Object.@class_identifier (00000110 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1297 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 1298 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1307 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1310 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object33={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1312 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object33={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 1316 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1320 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1322 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object33.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1327 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1331 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object33.@java.lang.Object.@class_identifier (00000110 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1346 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 1351 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1356 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1361 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1) State 1364 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1383 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.values:()[LMinePumpSystem/Environment$WaterLevelEnum; bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object18.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1386 thread 0 ---------------------------------------------------- dynamic_object34={ .@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 1388 thread 0 ---------------------------------------------------- dynamic_object34={ .@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 1389 thread 0 ---------------------------------------------------- dynamic_object34.length=3 (00000000 00000000 00000000 00000011) State 1392 thread 0 ---------------------------------------------------- dynamic_object34.data=dynamic_35_array (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1393 thread 0 ---------------------------------------------------- dynamic_35_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 1397 thread 0 ---------------------------------------------------- dynamic_35_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1401 thread 0 ---------------------------------------------------- dynamic_35_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1405 thread 0 ---------------------------------------------------- dynamic_35_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1425 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object36={ .@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 1427 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object36={ .@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 1428 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object36.length=3 (00000000 00000000 00000000 00000011) State 1431 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object36.data=dynamic_37_array (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1432 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_37_array={ 0, 0, 0 } ({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 }) State 1438 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 3 thread 0 ---------------------------------------------------- $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=&dynamic_object36.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1453 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1465 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 8 thread 0 ---------------------------------------------------- dynamic_37_array[2L]=1 (00000000 00000000 00000000 00000001) State 1481 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 (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1493 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 15 thread 0 ---------------------------------------------------- dynamic_37_array[1L]=2 (00000000 00000000 00000000 00000010) State 1509 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1521 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_37_array[0L]=3 (00000000 00000000 00000000 00000011) State 1531 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1552 file MinePumpSystem/Environment.java line 38 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object14.waterLevel=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1567 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1573 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1583 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1589 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1596 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 1604 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1612 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1618 file MinePumpSystem/MinePump.java line 54 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1624 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment__wrappee__lowWaterSensor:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1640 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1650 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1651 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1652 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1653 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1661 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1667 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1671 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1677 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1682 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1688 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1697 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1698 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1699 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1700 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1708 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1714 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1718 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1724 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1729 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1735 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1739 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 1746 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1747 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1748 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1749 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1751 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1760 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1766 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1770 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1776 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1781 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1787 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1791 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1805 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1816 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object42={ .@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 1818 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object42={ .@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 1822 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1826 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1830 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1834 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1836 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1840 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object42.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object42.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 assertion at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 false VERIFICATION FAILED EC=10 FALSE