./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/MinePump/spec1-5_product19_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.TOXv4c.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/MinePump/spec1-5_product19_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_product19_false-assert.jar JAR file without entry point: loading class files failed to load class `java.io.ObjectOutputStream' failed to load class `java.io.ObjectInputStream' failed to load class `java.io.PrintWriter' failed to load class `java.io.PrintStream' failed to load class `java.io.IOException' failed to load class `java.io.Serializable' failed to load class `java.lang.StackTraceElement' failed to load class `java.util.Objects' failed to load class `java.lang.AbstractStringBuilder' failed to load class `java.lang.invoke.MethodHandles' failed to load class `java.util.PrimitiveIterator' failed to load class `java.lang.invoke.LambdaMetafactory' failed to load class `java.lang.invoke.MethodHandle' failed to load class `java.lang.invoke.MethodType' failed to load class `java.lang.invoke.MethodHandles$Lookup' failed to load class `java.lang.invoke.CallSite' failed to load class `java.util.Spliterators' failed to load class `java.util.PrimitiveIterator$OfInt' failed to load class `java.util.Spliterator$OfInt' failed to load class `java.util.stream.StreamSupport' failed to load class `java.util.stream.IntStream' failed to load class `java.util.Spliterator' failed to load class `java.util.function.Supplier' failed to load class `java.util.NoSuchElementException' failed to load class `java.util.function.IntConsumer' failed to load class `java.lang.Comparable' failed to load class `java.util.Locale' failed to load class `java.lang.CharacterName' failed to load class `java.lang.CharacterData' failed to load class `java.lang.Byte' failed to load class `java.io.UnsupportedEncodingException' failed to load class `java.util.Comparator' failed to load class `java.lang.Iterable' failed to load class `java.util.Iterator' failed to load class `java.nio.charset.Charset' failed to load class `java.io.BufferedInputStream' failed to load class `java.lang.Number' failed to load class `java.lang.Long' failed to load class `java.lang.Appendable' failed to load class `java.util.HashMap' failed to load class `sun.reflect.Reflection' failed to load class `java.lang.System' failed to load class `java.lang.SecurityManager' failed to load class `java.lang.ClassLoader' failed to load class `java.util.Map' failed to load class `java.io.ObjectStreamException' failed to load class `java.io.InvalidObjectException' failed to load class `java.util.Arrays' failed to load class `java.util.stream.DoubleStream' failed to load class `java.util.stream.LongStream' Converting Method: java::java.lang.Object.getClass could not parse signature: ()Ljava/lang/Class<*>; Unsupported class signature: wild card generic reverting to descriptor: ()Ljava/lang/Class; Method: java::java.lang.String.join could not parse signature: (Ljava/lang/CharSequence;Ljava/lang/Iterable<+Ljava/lang/CharSequence;>;)Ljava/lang/String; Unsupported class signature: wild card generic reverting to descriptor: (Ljava/lang/CharSequence;Ljava/lang/Iterable;)Ljava/lang/String; Method: java::MinePumpSystem.Environment$WaterLevelEnum. signature: ()V descriptor: (Ljava/lang/String;I)V different number of parameters, reverting to descriptor Method: java::java.lang.Class.forName could not parse signature: (Ljava/lang/String;)Ljava/lang/Class<*>; Unsupported class signature: wild card generic reverting to descriptor: (Ljava/lang/String;)Ljava/lang/Class; Method: java::java.lang.Class.forName could not parse signature: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class<*>; Unsupported class signature: wild card generic reverting to descriptor: (Ljava/lang/String;ZLjava/lang/ClassLoader;)Ljava/lang/Class; Method: java::java.lang.Class.desiredAssertionStatus0 could not parse signature: (Ljava/lang/Class<*>;)Z Unsupported class signature: wild card generic reverting to descriptor: (Ljava/lang/Class;)Z Method: java::java.lang.Character$UnicodeScript. signature: ()V descriptor: (Ljava/lang/String;I)V different number of parameters, reverting to descriptor Class: java.lang.Enum could not parse signature: ;>Ljava/lang/Object;Ljava/lang/Comparable;Ljava/io/Serializable; Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum;>(Ljava/lang/Class;Ljava/lang/String;)TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: (Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum; Method: java::org.cprover.CProver.nondetWithNull could not parse signature: ()TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: ()Ljava/lang/Object; Method: java::org.cprover.CProver.nondetWithNull could not parse signature: (TT;)TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object; Method: java::org.cprover.CProver.nondetWithoutNull could not parse signature: ()TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: ()Ljava/lang/Object; Method: java::org.cprover.CProver.nondetWithoutNull could not parse signature: (TT;)TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object; Method: java::org.cprover.CProver.nondetWithNullForNotModelled could not parse signature: ()TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: ()Ljava/lang/Object; Method: java::org.cprover.CProver.nondetWithoutNullForNotModelled could not parse signature: ()TT; Unsupported class signature: Cannot currently parse bounds on generic types reverting to descriptor: ()Ljava/lang/Object; Java: added 2278 String or Class constant symbols Generating GOTO Program Running GOTO functions transformation passes Running with 11 object bits, 53 offset bits (user-specified) Starting Bounded Model Checking Unwinding loop __CPROVER__start.0 iteration 1 thread 0 Unwinding loop __CPROVER__start.0 iteration 2 thread 0 Unwinding loop __CPROVER__start.0 iteration 3 thread 0 Unwinding loop __CPROVER__start.0 iteration 4 thread 0 Unwinding loop __CPROVER__start.0 iteration 5 thread 0 Unwinding recursion java::Main::clinit_wrapper iteration 1 Unwinding recursion java::Actions::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$WaterLevelEnum::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.MinePump::clinit_wrapper iteration 1 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 1 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 96 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 2 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file MinePumpSystem/MinePump.java line 96 function java::MinePumpSystem.MinePump.stopSystem:()V bytecode-index 13 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.0 iteration 3 file Main.java line 48 function java::Main.randomSequenceOfActions:(I)V bytecode-index 41 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 1 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 1 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 2 thread 0 Unwinding loop java::array[reference].clone:()Ljava/lang/Object;.0 iteration 3 thread 0 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 Unwinding recursion java::MinePumpSystem.Environment$1::clinit_wrapper iteration 1 aborting path on assume(false) at file Actions.java line 71 function java::Actions.Specification1:()V bytecode-index 20 thread 0 aborting path on assume(false) at file Actions.java line 86 function java::Actions.Specification2:()V bytecode-index 23 thread 0 aborting path on assume(false) at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 thread 0 aborting path on assume(false) at file Actions.java line 119 function java::Actions.Specification4:()V bytecode-index 25 thread 0 aborting path on assume(false) at file Actions.java line 142 function java::Actions.Specification5_2:()V bytecode-index 28 thread 0 Unwinding loop java::Main.randomSequenceOfActions:(I)V.1 iteration 2 file Main.java line 50 function java::Main.randomSequenceOfActions:(I)V bytecode-index 50 thread 0 size of program expression: 45011 steps simple slicing removed 1 assignments Generated 393 VCC(s), 28 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 1958383 variables, 6157737 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 24.192s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .isAnnotation=false, .isArray=false, .isInterface=false, .isSynthetic=false, .isLocalClass=false, .isMemberClass=false, .isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 7 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 8 thread 0 ---------------------------------------------------- name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 9 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 10 thread 0 ---------------------------------------------------- isArray=false (00000000) State 11 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 12 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 13 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 14 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 15 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 17 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.name=&MinePumpSystem_2eMinePump.@java.lang.Object.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 19 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isAnnotation=false (00000000) State 21 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isArray=false (00000000) State 23 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isInterface=false (00000000) State 25 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isSynthetic=false (00000000) State 27 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isLocalClass=false (00000000) State 29 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isMemberClass=false (00000000) State 31 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0 ---------------------------------------------------- MinePumpSystem.MinePump@class_model.isEnum=false (00000000) State 34 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 35 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 36 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 37 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 38 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=false (0) State 39 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high_return_value=0 (00000000 00000000 00000000 00000000) State 40 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 41 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 43 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 44 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=3, .data=low_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 45 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_return_value=0 (00000000 00000000 00000000 00000000) State 46 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- low_constarray={ (char)'l', (char)'o', (char)'w' } ({ 00000000 01101100, 00000000 01101111, 00000000 01110111 }) State 47 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=6, .data=normal_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 48 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- normal_return_value=0 (00000000 00000000 00000000 00000000) State 49 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 50 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- high={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=4, .data=high_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 51 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 52 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 53 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- cleanupTimeShifts=0 (00000000 00000000 00000000 00000000) State 54 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 57 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 58 thread 0 ---------------------------------------------------- name=&Actions.@java.lang.Object.@class_identifier (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 59 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 60 thread 0 ---------------------------------------------------- isArray=false (00000000) State 61 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 62 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 63 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 64 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 65 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 67 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- Actions@class_model.name=&Actions.@java.lang.Object.@class_identifier (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 69 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 71 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 73 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 75 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 77 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 79 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 81 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 83 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 84 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=false (0) State 85 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=false (0) State 97 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 99 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 100 thread 0 ---------------------------------------------------- dynamic_object1.length=2 (00000000 00000000 00000000 00000010) State 103 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 104 thread 0 ---------------------------------------------------- dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 109 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 111 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 117 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 121 thread 0 ---------------------------------------------------- dynamic_object4={ } ( }) State 126 thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 127 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 132 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 134 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 140 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 144 thread 0 ---------------------------------------------------- dynamic_object6={ } ( }) State 149 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 150 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 154 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 157 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 161 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 168 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- cleanupTimeShifts=2 (00000000 00000000 00000000 00000010) State 173 file Main.java line 11 function java::Main.main:([Ljava/lang/String;)V bytecode-index 1 thread 0 ---------------------------------------------------- arg0i=3 (00000000 00000000 00000000 00000011) State 174 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 175 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 180 thread 0 ---------------------------------------------------- java$$Actions$$clinit_already_run=true (1) State 188 file Actions.java line 4 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 189 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 194 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 195 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 200 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 204 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 211 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 216 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&Actions@class_model.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 233 file Actions.java line 4 function java::Actions.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 238 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .env=null, .p=null, .methAndRunningLastTime=false, .switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 }) State 240 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::Actions", .cproverMonitorCount=0 }, .env=null, .p=null, .methAndRunningLastTime=false, .switchedOnBeforeTS=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000 }) State 244 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 250 file Actions.java line 14 function java::Actions.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 252 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object13.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 256 file Actions.java line 10 function java::Actions.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 258 file Actions.java line 11 function java::Actions.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 259 file Actions.java line 15 function java::Actions.:()V bytecode-index 9 thread 0 ---------------------------------------------------- dynamic_object14={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 }) State 261 file Actions.java line 15 function java::Actions.:()V bytecode-index 9 thread 0 ---------------------------------------------------- dynamic_object14={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment", .cproverMonitorCount=0 }, .waterLevel=null, .methaneLevelCritical=false } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 }) State 265 file Actions.java line 15 function java::Actions.:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 269 file MinePumpSystem/Environment.java line 3 function java::MinePumpSystem.Environment.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 271 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object14.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 277 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$WaterLevelEnum$$clinit_already_run=true (1) State 289 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 291 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object15={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 295 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 296 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg1a=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 297 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 4 thread 0 ---------------------------------------------------- arg2i=0 (00000000 00000000 00000000 00000000) State 301 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 302 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 303 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=0 (00000000 00000000 00000000 00000000) State 307 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 309 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object15.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 313 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object15.@java.lang.Enum.name=&low.@java.lang.Object.@class_identifier (00000110 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 315 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object15.@java.lang.Enum.ordinal=0 (00000000 00000000 00000000 00000000) State 325 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 5 thread 0 ---------------------------------------------------- low=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 331 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 6 thread 0 ---------------------------------------------------- dynamic_object16={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 333 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 6 thread 0 ---------------------------------------------------- dynamic_object16={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 337 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 338 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg1a=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 339 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 10 thread 0 ---------------------------------------------------- arg2i=1 (00000000 00000000 00000000 00000001) State 343 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 344 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 345 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=1 (00000000 00000000 00000000 00000001) State 349 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 351 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object16.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 355 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object16.@java.lang.Enum.name=&normal.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 357 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object16.@java.lang.Enum.ordinal=1 (00000000 00000000 00000000 00000001) State 367 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 11 thread 0 ---------------------------------------------------- normal=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 373 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object17={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 375 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object17={ .@java.lang.Enum={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.Environment$WaterLevelEnum", .cproverMonitorCount=0 }, .name=null, .ordinal=0 } } ({ { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 } }) State 379 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 380 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg1a=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 381 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 16 thread 0 ---------------------------------------------------- arg2i=2 (00000000 00000000 00000000 00000010) State 385 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 386 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 387 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:(Ljava/lang/String;I)V bytecode-index 3 thread 0 ---------------------------------------------------- ordinal=2 (00000000 00000000 00000000 00000010) State 391 file java/lang/Enum.java line 117 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 393 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object17.@java.lang.Enum.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 397 file java/lang/Enum.java line 118 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object17.@java.lang.Enum.name=&high.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 399 file java/lang/Enum.java line 119 function java::java.lang.Enum.:(Ljava/lang/String;I)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object17.@java.lang.Enum.ordinal=2 (00000000 00000000 00000000 00000010) State 409 file MinePumpSystem/Environment.java line 7 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 17 thread 0 ---------------------------------------------------- high=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 411 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 413 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 414 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.length=3 (00000000 00000000 00000000 00000011) State 417 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object18.data=dynamic_19_array (00000110 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 418 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_19_array={ null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 430 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 23 thread 0 ---------------------------------------------------- dynamic_19_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 442 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_19_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 454 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 31 thread 0 ---------------------------------------------------- dynamic_19_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 460 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.:()V bytecode-index 32 thread 0 ---------------------------------------------------- $VALUES=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 466 file MinePumpSystem/Environment.java line 11 function java::MinePumpSystem.Environment.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object14.waterLevel=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 468 file MinePumpSystem/Environment.java line 15 function java::MinePumpSystem.Environment.:()V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object14.methaneLevelCritical=false (00000000) State 472 file Actions.java line 15 function java::Actions.:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object13.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 476 thread 0 ---------------------------------------------------- java$$MinePumpSystem_MinePump$$clinit_already_run=true (1) State 484 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 485 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 490 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 491 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 496 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0 ---------------------------------------------------- this=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 500 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 507 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 512 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0 ---------------------------------------------------- clazz=&MinePumpSystem.MinePump@class_model.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 529 file MinePumpSystem/MinePump.java line 5 function java::MinePumpSystem.MinePump.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 534 file Actions.java line 16 function java::Actions.:()V bytecode-index 14 thread 0 ---------------------------------------------------- dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .pumpRunning=false, .systemActive=false, .env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 536 file Actions.java line 16 function java::Actions.:()V bytecode-index 14 thread 0 ---------------------------------------------------- dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::MinePumpSystem.MinePump", .cproverMonitorCount=0 }, .pumpRunning=false, .systemActive=false, .env=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 541 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 542 file Actions.java line 16 function java::Actions.:()V bytecode-index 18 thread 0 ---------------------------------------------------- arg1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 546 file MinePumpSystem/MinePump.java line 21 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 548 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 552 file MinePumpSystem/MinePump.java line 8 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object20.pumpRunning=false (00000000) State 554 file MinePumpSystem/MinePump.java line 12 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object20.systemActive=true (00000001) State 556 file MinePumpSystem/MinePump.java line 22 function java::MinePumpSystem.MinePump.:(LMinePumpSystem/Environment;)V bytecode-index 10 thread 0 ---------------------------------------------------- dynamic_object20.env=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 560 file Actions.java line 16 function java::Actions.:()V bytecode-index 19 thread 0 ---------------------------------------------------- dynamic_object13.p=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 563 file Main.java line 21 function java::Main.randomSequenceOfActions:(I)V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 564 file Main.java line 23 function java::Main.randomSequenceOfActions:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 566 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 567 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 568 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 569 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 573 file Main.java line 25 function java::Main.randomSequenceOfActions:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- anonlocal::2i=1 (00000000 00000000 00000000 00000001) State 580 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 583 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 585 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object21={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 589 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 593 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 595 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object21.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 600 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 604 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object21.@java.lang.Object.@class_identifier (00000110 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 619 file Main.java line 27 function java::Main.randomSequenceOfActions:(I)V bytecode-index 11 thread 0 ---------------------------------------------------- anonlocal::3i=1 (00000000 00000000 00000000 00000001) State 626 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 629 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 631 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object22={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 635 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 639 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 641 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object22.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 646 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 650 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object22.@java.lang.Object.@class_identifier (00000110 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 665 file Main.java line 28 function java::Main.randomSequenceOfActions:(I)V bytecode-index 13 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 672 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 675 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 677 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object23={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 681 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 685 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 687 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object23.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 692 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 696 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object23.@java.lang.Object.@class_identifier (00000111 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 711 file Main.java line 29 function java::Main.randomSequenceOfActions:(I)V bytecode-index 15 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 712 file Main.java line 30 function java::Main.randomSequenceOfActions:(I)V bytecode-index 17 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 721 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 724 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 726 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 0 thread 0 ---------------------------------------------------- dynamic_object24={ .@java.lang.Object={ .@class_identifier="java::java.util.Random", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } }) State 730 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 734 file java/util/Random.java line 116 function java::java.util.Random.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 736 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object24.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 741 file Main.java line 15 function java::Main.getBoolean:()Z bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::0a=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 745 file Main.java line 16 function java::Main.getBoolean:()Z bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object24.@java.lang.Object.@class_identifier (00000111 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 760 file Main.java line 31 function java::Main.randomSequenceOfActions:(I)V bytecode-index 21 thread 0 ---------------------------------------------------- anonlocal::6i=0 (00000000 00000000 00000000 00000000) State 765 file Main.java line 34 function java::Main.randomSequenceOfActions:(I)V bytecode-index 25 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 770 file Actions.java line 22 function java::Actions.waterRise:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 775 thread 0 ---------------------------------------------------- java$$MinePumpSystem_Environment$1$$clinit_already_run=true (1) State 778 thread 0 ---------------------------------------------------- anonlocal::0a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 797 file MinePumpSystem/Environment.java line 6 function java::MinePumpSystem.Environment$WaterLevelEnum.values:()[LMinePumpSystem/Environment$WaterLevelEnum; bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object18.@java.lang.Object.@class_identifier (00000110 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 800 thread 0 ---------------------------------------------------- dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 802 thread 0 ---------------------------------------------------- dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 803 thread 0 ---------------------------------------------------- dynamic_object25.length=3 (00000000 00000000 00000000 00000011) State 806 thread 0 ---------------------------------------------------- dynamic_object25.data=dynamic_26_array (00000111 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 807 thread 0 ---------------------------------------------------- dynamic_26_array={ null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 811 thread 0 ---------------------------------------------------- dynamic_26_array[0L]=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 815 thread 0 ---------------------------------------------------- dynamic_26_array[1L]=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 819 thread 0 ---------------------------------------------------- dynamic_26_array[2L]=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 839 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 841 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27={ .@java.lang.Object={ .@class_identifier="java::array[int]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 842 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27.length=3 (00000000 00000000 00000000 00000011) State 845 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object27.data=dynamic_28_array (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 846 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_28_array={ 0, 0, 0 } ({ 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 }) State 852 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 3 thread 0 ---------------------------------------------------- $SwitchMap$MinePumpSystem$Environment$WaterLevelEnum=&dynamic_object27.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 867 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 6 thread 0 ---------------------------------------------------- this=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 879 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 8 thread 0 ---------------------------------------------------- dynamic_28_array[2L]=1 (00000000 00000000 00000000 00000001) State 895 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 13 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 907 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 15 thread 0 ---------------------------------------------------- dynamic_28_array[1L]=2 (00000000 00000000 00000000 00000010) State 923 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 20 thread 0 ---------------------------------------------------- this=&dynamic_object15.@java.lang.Enum.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 935 file MinePumpSystem/Environment.java line 20 function java::MinePumpSystem.Environment$1.:()V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_28_array[0L]=3 (00000000 00000000 00000000 00000011) State 945 file MinePumpSystem/Environment.java line 33 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object16.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 966 file MinePumpSystem/Environment.java line 38 function java::MinePumpSystem.Environment.waterRise:()V bytecode-index 12 thread 0 ---------------------------------------------------- dynamic_object14.waterLevel=&dynamic_object17.@java.lang.Enum.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 981 file Main.java line 47 function java::Main.randomSequenceOfActions:(I)V bytecode-index 40 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 987 file Actions.java line 44 function java::Actions.timeShift:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 997 file Actions.java line 45 function java::Actions.timeShift:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1003 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1010 file Actions.java line 128 function java::Actions.Specification5_1:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object13.switchedOnBeforeTS=false (00000000) State 1018 file Actions.java line 47 function java::Actions.timeShift:()V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1026 file MinePumpSystem/MinePump.java line 31 function java::MinePumpSystem.MinePump.timeShift:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1032 file MinePumpSystem/MinePump.java line 45 function java::MinePumpSystem.MinePump.processEnvironment:()V bytecode-index 10 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1045 file Actions.java line 49 function java::Actions.timeShift:()V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1055 file Actions.java line 50 function java::Actions.timeShift:()V bytecode-index 14 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1056 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1057 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1058 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1066 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1072 file Actions.java line 65 function java::Actions.Specification1:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1076 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1082 file Actions.java line 67 function java::Actions.Specification1:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1087 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1093 file Actions.java line 68 function java::Actions.Specification1:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1102 file Actions.java line 51 function java::Actions.timeShift:()V bytecode-index 16 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1103 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1104 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1105 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1113 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1119 file Actions.java line 79 function java::Actions.Specification2:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1123 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1129 file Actions.java line 81 function java::Actions.Specification2:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1134 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1140 file Actions.java line 82 function java::Actions.Specification2:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1144 file Actions.java line 91 function java::Actions.Specification2:()V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_object13.methAndRunningLastTime=false (00000000) State 1151 file Actions.java line 52 function java::Actions.timeShift:()V bytecode-index 18 thread 0 ---------------------------------------------------- this=&dynamic_object13.@java.lang.Object.@class_identifier (00000110 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1152 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1153 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 1154 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1156 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1165 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1171 file Actions.java line 99 function java::Actions.Specification3:()V bytecode-index 3 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1175 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1181 file Actions.java line 101 function java::Actions.Specification3:()V bytecode-index 6 thread 0 ---------------------------------------------------- anonlocal::2i=0 (00000000 00000000 00000000 00000000) State 1186 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object20.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 1192 file Actions.java line 102 function java::Actions.Specification3:()V bytecode-index 10 thread 0 ---------------------------------------------------- anonlocal::3i=0 (00000000 00000000 00000000 00000000) State 1196 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 12 thread 0 ---------------------------------------------------- this=&dynamic_object14.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1210 file Actions.java line 103 function java::Actions.Specification3:()V bytecode-index 18 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 1221 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object78={ .@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 1223 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 27 thread 0 ---------------------------------------------------- dynamic_object78={ .@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 1227 file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1231 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1235 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1239 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 1241 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 1245 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object78.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object78.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 assertion at file Actions.java line 106 function java::Actions.Specification3:()V bytecode-index 30 false VERIFICATION FAILED EC=10 FALSE