./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/StaticCharMethods05_false-assert.jar
--------------------------------------------------------------------------------
./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.uMcpOq.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/StaticCharMethods05_false-assert.jar
Unwind: 11
JBMC version 5.9 (cbmc-5.7-5176-g7c4b5aa) 64-bit x86_64 linux
Parsing ../git-sv-benchmarks/java/jbmc-regression/StaticCharMethods05_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.io.InputStream'
failed to load class `java.util.Scanner'
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::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.<init>
signature: ()V
descriptor: (Ljava/lang/String;I)V
different number of parameters, reverting to descriptor
Class: java.lang.Enum
could not parse signature: <E:Ljava/lang/Enum<TE;>;>Ljava/lang/Object;Ljava/lang/Comparable<TE;>;Ljava/io/Serializable;
Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum<TE
ignoring that the class is generic
Method: java::java.lang.Enum.valueOf
could not parse signature: <T:Ljava/lang/Enum<TT;>;>(Ljava/lang/Class<TT;>;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: <T:Ljava/lang/Object;>()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: <T:Ljava/lang/Object;>(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: <T:Ljava/lang/Object;>()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: <T:Ljava/lang/Object;>(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: <T:Ljava/lang/Object;>()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: <T:Ljava/lang/Object;>()TT;
Unsupported class signature: Cannot currently parse bounds on generic types
reverting to descriptor: ()Ljava/lang/Object;
Java: added 2231 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
aborting path on assume(false) at file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 23 thread 0
Unwinding recursion java::java.lang.Character::clinit_wrapper iteration 1
aborting path on assume(false) at file java/lang/Class.java line 334 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 64 thread 0
Unwinding recursion java::java.lang.Character::clinit_wrapper iteration 1
aborting path on assume(false) at file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 57 thread 0
Unwinding recursion java::java.lang.Character::clinit_wrapper iteration 1
aborting path on assume(false) at file java/lang/Class.java line 334 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 64 thread 0
Unwinding recursion java::java.lang.Character::clinit_wrapper iteration 1
Unwinding recursion java::java.lang.Integer::clinit_wrapper iteration 1
size of program expression: 5813 steps
simple slicing removed 1 assignments
Generated 9 VCC(s), 3 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
warning: ignoring array
* type: array
* size: constant
* type: signedbv
* width: 32
* #c_type: signed_int
* value: 00000000000000000000000000000000
0: unsignedbv
* width: 16
warning: ignoring <
* type: bool
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: +
* type: unsignedbv
* width: 16
0: constant
* type: unsignedbv
* width: 16
* value: 1111111111010000
1: typecast
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1#8
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i
* #source_location:
* file: Main.java
* line: 34
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 65
* #base_name: anonlocal::6i
* L0: 0
* L1: 1
* L2: 8
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1
* #SSA_symbol: 1
1: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1#11
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i
* #source_location:
* file: Main.java
* line: 16
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 7
* #base_name: anonlocal::2i
* L0: 0
* L1: 1
* L2: 11
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1
* #SSA_symbol: 1
warning: ignoring <
* type: bool
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: +
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: constant
* type: unsignedbv
* width: 16
* value: 1111111111001001
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
1: typecast
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1#8
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i
* #source_location:
* file: Main.java
* line: 34
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 65
* #base_name: anonlocal::6i
* L0: 0
* L1: 1
* L2: 8
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1
* #SSA_symbol: 1
1: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1#11
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i
* #source_location:
* file: Main.java
* line: 16
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 7
* #base_name: anonlocal::2i
* L0: 0
* L1: 1
* L2: 11
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1
* #SSA_symbol: 1
warning: ignoring <
* type: bool
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: +
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: constant
* type: unsignedbv
* width: 16
* value: 1111111110101001
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
1: typecast
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1#8
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i
* #source_location:
* file: Main.java
* line: 34
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 65
* #base_name: anonlocal::6i
* L0: 0
* L1: 1
* L2: 8
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1
* #SSA_symbol: 1
1: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1#11
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i
* #source_location:
* file: Main.java
* line: 16
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 7
* #base_name: anonlocal::2i
* L0: 0
* L1: 1
* L2: 11
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1
* #SSA_symbol: 1
warning: ignoring <
* type: bool
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: +
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: constant
* type: unsignedbv
* width: 16
* value: 0000000011101001
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
1: typecast
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1#8
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i
* #source_location:
* file: Main.java
* line: 34
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 65
* #base_name: anonlocal::6i
* L0: 0
* L1: 1
* L2: 8
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1
* #SSA_symbol: 1
1: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1#11
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i
* #source_location:
* file: Main.java
* line: 16
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 7
* #base_name: anonlocal::2i
* L0: 0
* L1: 1
* L2: 11
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1
* #SSA_symbol: 1
warning: ignoring <
* type: bool
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: +
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: constant
* type: unsignedbv
* width: 16
* value: 0000000011001001
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
1: typecast
* type: unsignedbv
* width: 16
* #source_location:
* file: Main.java
* line: 36
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 74
0: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1#8
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i
* #source_location:
* file: Main.java
* line: 34
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 65
* #base_name: anonlocal::6i
* L0: 0
* L1: 1
* L2: 8
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::6i!0@1
* #SSA_symbol: 1
1: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1#11
* expression: symbol
* type: signedbv
* width: 32
* #c_type: signed_int
* identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i
* #source_location:
* file: Main.java
* line: 16
* function: java::Main.main:([Ljava/lang/String;)V
* java_bytecode_index: 7
* #base_name: anonlocal::2i
* L0: 0
* L1: 1
* L2: 11
* L1_object_identifier: java::Main.main:([Ljava/lang/String;)V::anonlocal::2i!0@1
* #SSA_symbol: 1
BV-Refinement: post-processing
BV-Refinement: iteration 1
123951 variables, 221855 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
BV-Refinement: post-processing
BV-Refinement: iteration 1
124019 variables, 191948 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime decision procedure: 0.406885s
Building error trace
Counterexample:
State 3 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000)
State 4 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=false (0)
State 5 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
String_20index_20out_20of_20range_3a_20_constarray={ (char)'S', (char)'t', (char)'r', (char)'i', (char)'n', (char)'g', (char)' ', (char)'i', (char)'n', (char)'d', (char)'e', (char)'x', (char)' ', (char)'o', (char)'u', (char)'t', (char)' ', (char)'o', (char)'f', (char)' ', (char)'r', (char)'a', (char)'n', (char)'g', (char)'e', (char)':', (char)' ' } ({ 00000000 01010011, 00000000 01110100, 00000000 01110010, 00000000 01101001, 00000000 01101110, 00000000 01100111, 00000000 00100000, 00000000 01101001, 00000000 01101110, 00000000 01100100, 00000000 01100101, 00000000 01111000, 00000000 00100000, 00000000 01101111, 00000000 01110101, 00000000 01110100, 00000000 00100000, 00000000 01101111, 00000000 01100110, 00000000 00100000, 00000000 01110010, 00000000 01100001, 00000000 01101110, 00000000 01100111, 00000000 01100101, 00000000 00111010, 00000000 00100000 })
State 6 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
out=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 7 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
in=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 8 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20character_3a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=18, .data=Enter_20a_20character_3a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00010010, 00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 9 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void_constarray={ (char)'v', (char)'o', (char)'i', (char)'d' } ({ 00000000 01110110, 00000000 01101111, 00000000 01101001, 00000000 01100100 })
State 10 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double_constarray={ (char)'d', (char)'o', (char)'u', (char)'b', (char)'l', (char)'e' } ({ 00000000 01100100, 00000000 01101111, 00000000 01110101, 00000000 01100010, 00000000 01101100, 00000000 01100101 })
State 11 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double_return_value=0 (00000000 00000000 00000000 00000000)
State 12 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=6, .data=double_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 13 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float_constarray={ (char)'f', (char)'l', (char)'o', (char)'a', (char)'t' } ({ 00000000 01100110, 00000000 01101100, 00000000 01101111, 00000000 01100001, 00000000 01110100 })
State 14 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=long_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 15 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int_constarray={ (char)'i', (char)'n', (char)'t' } ({ 00000000 01101001, 00000000 01101110, 00000000 01110100 })
State 16 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int_return_value=0 (00000000 00000000 00000000 00000000)
State 17 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=3, .data=int_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 18 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short_constarray={ (char)'s', (char)'h', (char)'o', (char)'r', (char)'t' } ({ 00000000 01110011, 00000000 01101000, 00000000 01101111, 00000000 01110010, 00000000 01110100 })
State 19 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=5, .data=short_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000101, 00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 20 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean_return_value=0 (00000000 00000000 00000000 00000000)
State 21 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=7, .data=boolean_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000111, 00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 22 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=void_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 23 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void_return_value=0 (00000000 00000000 00000000 00000000)
State 24 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long_return_value=0 (00000000 00000000 00000000 00000000)
State 25 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_Integer$$clinit_already_run=false (0)
State 26 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=5, .data=float_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000101, 00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 27 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20digit_3a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=14, .data=Enter_20a_20digit_3a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001110, 00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 28 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long_constarray={ (char)'l', (char)'o', (char)'n', (char)'g' } ({ 00000000 01101100, 00000000 01101111, 00000000 01101110, 00000000 01100111 })
State 29 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20character_3a_return_value=0 (00000000 00000000 00000000 00000000)
State 30 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=byte_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 31 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
_constarray={ } ( })
State 32 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float_return_value=0 (00000000 00000000 00000000 00000000)
State 34 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
TYPE=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 35 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean_constarray={ (char)'b', (char)'o', (char)'o', (char)'l', (char)'e', (char)'a', (char)'n' } ({ 00000000 01100010, 00000000 01101111, 00000000 01101111, 00000000 01101100, 00000000 01100101, 00000000 01100001, 00000000 01101110 })
State 36 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short_return_value=0 (00000000 00000000 00000000 00000000)
State 37 thread 0
----------------------------------------------------
java.lang.Character@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 40 thread 0
----------------------------------------------------
this=&java.lang.Character@class_model.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 41 thread 0
----------------------------------------------------
name=&java_2elang_2eCharacter.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 42 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 43 thread 0
----------------------------------------------------
isArray=false (00000000)
State 44 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 45 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 46 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 47 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 48 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 50 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
java.lang.Character@class_model.name=&java_2elang_2eCharacter.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 52 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0
----------------------------------------------------
java.lang.Character@class_model.isAnnotation=false (00000000)
State 54 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0
----------------------------------------------------
java.lang.Character@class_model.isArray=false (00000000)
State 56 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0
----------------------------------------------------
java.lang.Character@class_model.isInterface=false (00000000)
State 58 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0
----------------------------------------------------
java.lang.Character@class_model.isSynthetic=false (00000000)
State 60 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0
----------------------------------------------------
java.lang.Character@class_model.isLocalClass=false (00000000)
State 62 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0
----------------------------------------------------
java.lang.Character@class_model.isMemberClass=false (00000000)
State 64 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0
----------------------------------------------------
java.lang.Character@class_model.isEnum=false (00000000)
State 66 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte_return_value=0 (00000000 00000000 00000000 00000000)
State 67 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
CASE_INSENSITIVE_ORDER=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 68 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=char_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 69 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char_return_value=0 (00000000 00000000 00000000 00000000)
State 70 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char_constarray={ (char)'c', (char)'h', (char)'a', (char)'r' } ({ 00000000 01100011, 00000000 01101000, 00000000 01100001, 00000000 01110010 })
State 71 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_String$$clinit_already_run=false (0)
State 72 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20digit_3a_constarray={ (char)'E', (char)'n', (char)'t', (char)'e', (char)'r', (char)' ', (char)'a', (char)' ', (char)'d', (char)'i', (char)'g', (char)'i', (char)'t', (char)':' } ({ 00000000 01000101, 00000000 01101110, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00100000, 00000000 01100001, 00000000 00100000, 00000000 01100100, 00000000 01101001, 00000000 01100111, 00000000 01101001, 00000000 01110100, 00000000 00111010 })
State 73 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 74 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
TYPE=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 75 thread 0
----------------------------------------------------
Main@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 78 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 79 thread 0
----------------------------------------------------
name=&Main.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 80 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 81 thread 0
----------------------------------------------------
isArray=false (00000000)
State 82 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 83 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 84 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 85 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 86 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 88 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
Main@class_model.name=&Main.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 90 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0
----------------------------------------------------
Main@class_model.isAnnotation=false (00000000)
State 92 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0
----------------------------------------------------
Main@class_model.isArray=false (00000000)
State 94 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0
----------------------------------------------------
Main@class_model.isInterface=false (00000000)
State 96 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0
----------------------------------------------------
Main@class_model.isSynthetic=false (00000000)
State 98 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0
----------------------------------------------------
Main@class_model.isLocalClass=false (00000000)
State 100 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0
----------------------------------------------------
Main@class_model.isMemberClass=false (00000000)
State 102 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0
----------------------------------------------------
Main@class_model.isEnum=false (00000000)
State 104 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte_constarray={ (char)'b', (char)'y', (char)'t', (char)'e' } ({ 00000000 01100010, 00000000 01111001, 00000000 01110100, 00000000 01100101 })
State 105 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_System$$clinit_already_run=false (0)
State 106 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
String_20index_20out_20of_20range_3a_20_return_value=0 (00000000 00000000 00000000 00000000)
State 107 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20character_20to_20digit_3a_20_25s_0a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=31, .data=Convert_20character_20to_20digit_3a_20_25s_0a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011111, 00000010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 108 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java.lang.String.Literal.={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000010 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 109 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
_return_value=0 (00000000 00000000 00000000 00000000)
State 110 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
String_20index_20out_20of_20range_3a_20={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=27, .data=String_20index_20out_20of_20range_3a_20_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011011, 00000010 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 111 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20digit_3a_return_value=0 (00000000 00000000 00000000 00000000)
State 112 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 113 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20digit_20to_20character_3a_20_25s_0a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=31, .data=Convert_20digit_20to_20character_3a_20_25s_0a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011111, 00000010 10000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 114 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20digit_20to_20character_3a_20_25s_0a_return_value=0 (00000000 00000000 00000000 00000000)
State 115 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20digit_20to_20character_3a_20_25s_0a_constarray={ (char)'C', (char)'o', (char)'n', (char)'v', (char)'e', (char)'r', (char)'t', (char)' ', (char)'d', (char)'i', (char)'g', (char)'i', (char)'t', (char)' ', (char)'t', (char)'o', (char)' ', (char)'c', (char)'h', (char)'a', (char)'r', (char)'a', (char)'c', (char)'t', (char)'e', (char)'r', (char)':', (char)' ', (char)'%', (char)'s', (char)'\n' } ({ 00000000 01000011, 00000000 01101111, 00000000 01101110, 00000000 01110110, 00000000 01100101, 00000000 01110010, 00000000 01110100, 00000000 00100000, 00000000 01100100, 00000000 01101001, 00000000 01100111, 00000000 01101001, 00000000 01110100, 00000000 00100000, 00000000 01110100, 00000000 01101111, 00000000 00100000, 00000000 01100011, 00000000 01101000, 00000000 01100001, 00000000 01110010, 00000000 01100001, 00000000 01100011, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00111010, 00000000 00100000, 00000000 00100101, 00000000 01110011, 00000000 00001010 })
State 116 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Enter_20a_20character_3a_constarray={ (char)'E', (char)'n', (char)'t', (char)'e', (char)'r', (char)' ', (char)'a', (char)' ', (char)'c', (char)'h', (char)'a', (char)'r', (char)'a', (char)'c', (char)'t', (char)'e', (char)'r', (char)':' } ({ 00000000 01000101, 00000000 01101110, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00100000, 00000000 01100001, 00000000 00100000, 00000000 01100011, 00000000 01101000, 00000000 01100001, 00000000 01110010, 00000000 01100001, 00000000 01100011, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00111010 })
State 117 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20character_20to_20digit_3a_20_25s_0a_return_value=0 (00000000 00000000 00000000 00000000)
State 118 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
Convert_20character_20to_20digit_3a_20_25s_0a_constarray={ (char)'C', (char)'o', (char)'n', (char)'v', (char)'e', (char)'r', (char)'t', (char)' ', (char)'c', (char)'h', (char)'a', (char)'r', (char)'a', (char)'c', (char)'t', (char)'e', (char)'r', (char)' ', (char)'t', (char)'o', (char)' ', (char)'d', (char)'i', (char)'g', (char)'i', (char)'t', (char)':', (char)' ', (char)'%', (char)'s', (char)'\n' } ({ 00000000 01000011, 00000000 01101111, 00000000 01101110, 00000000 01110110, 00000000 01100101, 00000000 01110010, 00000000 01110100, 00000000 00100000, 00000000 01100011, 00000000 01101000, 00000000 01100001, 00000000 01110010, 00000000 01100001, 00000000 01100011, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00100000, 00000000 01110100, 00000000 01101111, 00000000 00100000, 00000000 01100100, 00000000 01101001, 00000000 01100111, 00000000 01101001, 00000000 01110100, 00000000 00111010, 00000000 00100000, 00000000 00100101, 00000000 01110011, 00000000 00001010 })
State 119 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_Character$$clinit_already_run=false (0)
State 131 thread 0
----------------------------------------------------
dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 133 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 134 thread 0
----------------------------------------------------
dynamic_object1.length=1 (00000000 00000000 00000000 00000001)
State 137 thread 0
----------------------------------------------------
dynamic_object1.data=dynamic_2_array (00000010 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 138 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 143 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 145 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000010 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 151 thread 0
----------------------------------------------------
dynamic_object4=dynamic_object4#1 (?)
State 155 thread 0
----------------------------------------------------
dynamic_object4={ } ( })
State 160 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, 00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 161 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 165 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000010 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 168 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000010 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 169 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 170 thread 0
----------------------------------------------------
anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 171 thread 0
----------------------------------------------------
anonlocal::3i=0 (00000000 00000000 00000000 00000000)
State 175 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@class_identifier="java::java.lang.String" } ({ ? })
State 177 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@class_identifier="java::java.util.Scanner" } ({ ? })
State 181 thread 0
----------------------------------------------------
java$$java_lang_System$$clinit_already_run=true (1)
State 185 thread 0
----------------------------------------------------
dynamic_object14={ .@class_identifier="java::java.lang.String" } ({ ? })
State 187 thread 0
----------------------------------------------------
in=&dynamic_object14.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 188 thread 0
----------------------------------------------------
dynamic_object14={ .@class_identifier="java::java.io.InputStream" } ({ ? })
State 190 thread 0
----------------------------------------------------
dynamic_object15={ .@class_identifier="java::java.lang.String" } ({ ? })
State 192 thread 0
----------------------------------------------------
out=&dynamic_object15.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 193 thread 0
----------------------------------------------------
dynamic_object15={ .@class_identifier="java::java.io.PrintStream" } ({ ? })
State 199 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object13.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 200 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V bytecode-index 3 thread 0
----------------------------------------------------
stub_ignored_arg1=&dynamic_object14.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 203 file Main.java line 14 function java::Main.main:([Ljava/lang/String;)V bytecode-index 4 thread 0
----------------------------------------------------
anonlocal::1a=&dynamic_object13.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 207 file Main.java line 16 function java::Main.main:([Ljava/lang/String;)V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object13.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 212 file Main.java line 16 function java::Main.main:([Ljava/lang/String;)V bytecode-index 7 thread 0
----------------------------------------------------
anonlocal::2i=0 (00000000 00000000 00000000 00000000)
State 216 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object13.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 222 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 12 thread 0
----------------------------------------------------
anonlocal::3i=1 (00000000 00000000 00000000 00000001)
State 226 thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=true (1)
State 234 file Main.java line 10 function java::Main.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 235 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 240 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 241 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 246 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 250 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 257 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 262 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
clazz=&Main@class_model.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 279 file Main.java line 10 function java::Main.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 290 thread 0
----------------------------------------------------
anonlocal::5i=0 (00000000 00000000 00000000 00000000)
State 291 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 305 file Main.java line 24 function java::Main.main:([Ljava/lang/String;)V bytecode-index 28 thread 0
----------------------------------------------------
this=&dynamic_object15.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 306 file Main.java line 24 function java::Main.main:([Ljava/lang/String;)V bytecode-index 28 thread 0
----------------------------------------------------
stub_ignored_arg1=&Enter_20a_20digit_3a.@java.lang.Object.@class_identifier (00000100 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 311 file Main.java line 25 function java::Main.main:([Ljava/lang/String;)V bytecode-index 30 thread 0
----------------------------------------------------
this=&dynamic_object13.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 316 file Main.java line 25 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0
----------------------------------------------------
anonlocal::4i=0 (00000000 00000000 00000000 00000000)
State 322 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0
----------------------------------------------------
dynamic_object17={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 324 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0
----------------------------------------------------
dynamic_object17={ .@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 325 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0
----------------------------------------------------
dynamic_object17.length=1 (00000000 00000000 00000000 00000001)
State 328 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0
----------------------------------------------------
dynamic_object17.data=dynamic_18_array (00000100 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 329 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0
----------------------------------------------------
dynamic_18_array={ null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 333 thread 0
----------------------------------------------------
java$$java_lang_Character$$clinit_already_run=true (1)
State 341 file java/lang/Character.java line 122 function java::java.lang.Character.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&java.lang.Character@class_model.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 342 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 347 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
this=&java.lang.Character@class_model.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 348 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 353 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
this=&java.lang.Character@class_model.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 357 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 364 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 369 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
clazz=&java.lang.Character@class_model.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 387 file java/lang/Character.java line 122 function java::java.lang.Character.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 390 file java/lang/Character.java line 175 function java::java.lang.Character.<clinit>:()V bytecode-index 8 thread 0
----------------------------------------------------
s=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 395 file java/lang/Class.java line 313 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 2 thread 0
----------------------------------------------------
this=&boolean.@java.lang.Object.@class_identifier (00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 396 file java/lang/Class.java line 313 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 2 thread 0
----------------------------------------------------
anObject=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 430 file java/lang/Class.java line 315 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 9 thread 0
----------------------------------------------------
this=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 431 file java/lang/Class.java line 315 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 9 thread 0
----------------------------------------------------
anObject=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 463 file java/lang/Class.java line 316 function java::java.lang.Class.getPrimitiveClass:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 12 thread 0
----------------------------------------------------
className=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 465 thread 0
----------------------------------------------------
c=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 466 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object20={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.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 468 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object20={ .@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 472 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 476 file java/lang/Class.java line 39 function java::java.lang.Class.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object20.@java.lang.Object.@class_identifier (00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 478 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object20.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 482 file java/lang/Class.java line 377 function java::java.lang.Class.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object20.enumConstantDirectory=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 485 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 3 thread 0
----------------------------------------------------
c=&dynamic_object20.@java.lang.Object.@class_identifier (00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 487 file java/lang/Class.java line 110 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 6 thread 0
----------------------------------------------------
dynamic_object20.name=&char.@java.lang.Object.@class_identifier (00000101 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 502 file java/lang/Character.java line 175 function java::java.lang.Character.<clinit>:()V bytecode-index 9 thread 0
----------------------------------------------------
TYPE=&dynamic_object20.@java.lang.Object.@class_identifier (00000101 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 515 file Main.java line 27 function java::Main.main:([Ljava/lang/String;)V bytecode-index 41 thread 0
----------------------------------------------------
c=(char)'0' (00000000 00110000)
State 522 file java/lang/Character.java line 4577 function java::java.lang.Character.valueOf:(C)Ljava/lang/Character; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object29={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.value=(char)'\u0000' } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 })
State 524 file java/lang/Character.java line 4577 function java::java.lang.Character.valueOf:(C)Ljava/lang/Character; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object29={ .@java.lang.Object={ .@class_identifier="java::java.lang.Character",
.cproverMonitorCount=0 },
.value=(char)'\u0000' } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 })
State 528 file java/lang/Character.java line 4577 function java::java.lang.Character.valueOf:(C)Ljava/lang/Character; bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object29.@java.lang.Object.@class_identifier (00000111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 529 file java/lang/Character.java line 4577 function java::java.lang.Character.valueOf:(C)Ljava/lang/Character; bytecode-index 3 thread 0
----------------------------------------------------
value=(char)'0' (00000000 00110000)
State 533 file java/lang/Character.java line 4537 function java::java.lang.Character.<init>:(C)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object29.@java.lang.Object.@class_identifier (00000111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 535 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object29.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 539 file java/lang/Character.java line 4538 function java::java.lang.Character.<init>:(C)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object29.value=(char)'0' (00000000 00110000)
State 552 file Main.java line 27 function java::Main.main:([Ljava/lang/String;)V bytecode-index 42 thread 0
----------------------------------------------------
dynamic_18_array[0L]=&dynamic_object29.@java.lang.Object.@class_identifier (00000111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 556 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 43 thread 0
----------------------------------------------------
this=&dynamic_object15.@class_identifier (00000100 01100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 557 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 43 thread 0
----------------------------------------------------
stub_ignored_arg1=&Convert_20digit_20to_20character_3a_20_25s_0a.@java.lang.Object.@class_identifier (00000111 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 558 file Main.java line 26 function java::Main.main:([Ljava/lang/String;)V bytecode-index 43 thread 0
----------------------------------------------------
stub_ignored_arg2=&dynamic_object17.@java.lang.Object.@class_identifier (00000100 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 572 file Main.java line 28 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0
----------------------------------------------------
anonlocal::5i=48 (00000000 00000000 00000000 00110000)
State 581 file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 54 thread 0
----------------------------------------------------
dynamic_object31={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.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 583 file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 54 thread 0
----------------------------------------------------
dynamic_object31={ .@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 587 file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 56 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 591 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 595 file java/lang/Error.java line 58 function java::java.lang.Error.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 599 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 601 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 605 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object31.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object31.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000111 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
Violated property:
file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 57
assertion at file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 57
false
VERIFICATION FAILED
EC=10
FALSE