./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/StringMiscellaneous03_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.BeabIG.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/StringMiscellaneous03_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/StringMiscellaneous03_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' 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. 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 2219 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 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 1 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 2 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 3 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 4 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 5 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 6 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 7 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 8 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 9 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 10 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 Not unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 11 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 size of program expression: 46230 steps simple slicing removed 1 assignments Generated 213 VCC(s), 12 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 976954 variables, 2722242 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 516.427s Building error trace Counterexample: State 3 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000) State 4 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 5 file Main.java line 12 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 12 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, 00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 8 file Main.java line 12 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 9 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 10 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- CASE_INSENSITIVE_ORDER=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 11 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 14 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 15 thread 0 ---------------------------------------------------- name=&Main.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 16 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 17 thread 0 ---------------------------------------------------- isArray=false (00000000) State 18 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 19 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 20 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 21 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 22 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 24 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 (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 26 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 28 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 30 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 32 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 34 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 36 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 38 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 40 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$java_lang_String$$clinit_already_run=false (0) State 52 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 54 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 55 thread 0 ---------------------------------------------------- dynamic_object1.length=5 (00000000 00000000 00000000 00000101) State 58 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 59 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 64 file Main.java line 12 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 66 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[0L]=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 72 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 76 thread 0 ---------------------------------------------------- dynamic_object4={ (char)'\u547e', (char)'\u77c7', (char)'\u3acb', (char)'\u566f', (char)'\u9b5b', (char)'\u3acb', (char)'\ue3d0', (char)'\u0bde', (char)'\u3ac7' } ({ 01010100 01111110, 01110111 11000111, 00111010 11001011, 01010110 01101111, 10011011 01011011, 00111010 11001011, 11100011 11010000, 00001011 11011110, 00111010 11000111 }) State 81 thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=9, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001001, 00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 82 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object3.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 87 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5={ .@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 89 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[1L]=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 95 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 99 thread 0 ---------------------------------------------------- dynamic_object6={ (char)'\ua017' } ({ 10100000 00010111 }) State 104 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=1, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000001, 00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 105 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object5.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 110 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object7={ .@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 112 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[2L]=&dynamic_object7.@java.lang.Object.@class_identifier (00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 118 thread 0 ---------------------------------------------------- dynamic_object8=dynamic_object8#1 (?) State 122 thread 0 ---------------------------------------------------- dynamic_object8={ } ( }) State 127 thread 0 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 128 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object7.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 133 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object9={ .@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 135 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[3L]=&dynamic_object9.@java.lang.Object.@class_identifier (00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 141 thread 0 ---------------------------------------------------- dynamic_object10=dynamic_object10#1 (?) State 145 thread 0 ---------------------------------------------------- dynamic_object10={ (char)'\ua48c', (char)'\u0672', (char)'\u32f9', (char)'\u4c32', (char)'\u4233', (char)'\u90e9' } ({ 10100100 10001100, 00000110 01110010, 00110010 11111001, 01001100 00110010, 01000010 00110011, 10010000 11101001 }) State 150 thread 0 ---------------------------------------------------- dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=6, .data=dynamic_object10 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 151 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object9.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 156 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object11={ .@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 158 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[4L]=&dynamic_object11.@java.lang.Object.@class_identifier (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 164 thread 0 ---------------------------------------------------- dynamic_object12=dynamic_object12#1 (?) State 168 thread 0 ---------------------------------------------------- dynamic_object12={ (char)'\u5095', (char)'\ub06c', (char)'\ue5d8', (char)'\uf9dd', (char)'l', (char)'\u75dc', (char)'\u4cdd', (char)'\u7249', (char)'\u2bff', (char)'\u68b7', (char)'\u0bdb', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?', (char)'?' } ({ 01010000 10010101, 10110000 01101100, 11100101 11011000, 11111001 11011101, 00000000 01101100, 01110101 11011100, 01001100 11011101, 01110010 01001001, 00101011 11111111, 01101000 10110111, 00001011 11011011, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111, 00000000 00111111 }) State 173 thread 0 ---------------------------------------------------- dynamic_object11={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=38, .data=dynamic_object12 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00100110, 00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 174 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_object11.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 178 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 181 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 198 thread 0 ---------------------------------------------------- anonlocal::5i=0 (00000000 00000000 00000000 00000000) State 199 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 200 thread 0 ---------------------------------------------------- anonlocal::2a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 201 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 202 thread 0 ---------------------------------------------------- anonlocal::3a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 211 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 218 file Main.java line 16 function java::Main.main:([Ljava/lang/String;)V bytecode-index 20 thread 0 ---------------------------------------------------- anonlocal::2a=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 220 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 22 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 222 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_object17={ .@java.lang.Object={ .@class_identifier="java::array[char]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 223 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_object17.length=5 (00000000 00000000 00000000 00000101) State 226 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_object17.data=dynamic_18_array (?) State 227 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 22 thread 0 ---------------------------------------------------- dynamic_18_array={ (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000' } ({ 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000 }) State 228 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 23 thread 0 ---------------------------------------------------- anonlocal::3a=&dynamic_object17.@java.lang.Object.@class_identifier (00000010 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 229 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 25 thread 0 ---------------------------------------------------- anonlocal::4i=0 (00000000 00000000 00000000 00000000) State 233 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 27 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 239 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 30 thread 0 ---------------------------------------------------- anonlocal::5i=8 (00000000 00000000 00000000 00001000) State 244 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 252 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 253 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 258 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 259 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 264 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 268 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 275 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 280 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 (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 297 file Main.java line 8 function java::Main.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 308 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 37 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 309 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 37 thread 0 ---------------------------------------------------- index=8 (00000000 00000000 00000000 00001000) State 315 file java/lang/String.java line 768 function java::java.lang.String.charAt:(I)C bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 326 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- s=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 327 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=8 (00000000 00000000 00000000 00001000) State 348 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 40 thread 0 ---------------------------------------------------- this=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 349 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 40 thread 0 ---------------------------------------------------- index=0 (00000000 00000000 00000000 00000000) State 355 file java/lang/String.java line 768 function java::java.lang.String.charAt:(I)C bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 366 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- s=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 367 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=0 (00000000 00000000 00000000 00000000) State 387 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 46 thread 0 ---------------------------------------------------- anonlocal::4i=1 (00000000 00000000 00000000 00000001) State 388 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 47 thread 0 ---------------------------------------------------- anonlocal::5i=7 (00000000 00000000 00000000 00000111) State 402 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 37 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 403 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 37 thread 0 ---------------------------------------------------- index=7 (00000000 00000000 00000000 00000111) State 409 file java/lang/String.java line 768 function java::java.lang.String.charAt:(I)C bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 420 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- s=&dynamic_object3.@java.lang.Object.@class_identifier (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 421 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=7 (00000000 00000000 00000000 00000111) State 442 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 40 thread 0 ---------------------------------------------------- this=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 443 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 40 thread 0 ---------------------------------------------------- index=1 (00000000 00000000 00000000 00000001) State 449 file java/lang/String.java line 768 function java::java.lang.String.charAt:(I)C bytecode-index 4 thread 0 ---------------------------------------------------- this=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 457 file java/lang/String.java line 769 function java::java.lang.String.charAt:(I)C bytecode-index 6 thread 0 ---------------------------------------------------- dynamic_object61={ .@java.lang.IndexOutOfBoundsException={ .@java.lang.RuntimeException={ .@java.lang.Exception={ .@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 459 file java/lang/String.java line 769 function java::java.lang.String.charAt:(I)C bytecode-index 6 thread 0 ---------------------------------------------------- dynamic_object61={ .@java.lang.IndexOutOfBoundsException={ .@java.lang.RuntimeException={ .@java.lang.Exception={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.StringIndexOutOfBoundsException", .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 463 file java/lang/String.java line 769 function java::java.lang.String.charAt:(I)C bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 464 file java/lang/String.java line 769 function java::java.lang.String.charAt:(I)C bytecode-index 9 thread 0 ---------------------------------------------------- index=1 (00000000 00000000 00000000 00000001) State 469 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 1 thread 0 ---------------------------------------------------- dynamic_object62={ .@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 471 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 1 thread 0 ---------------------------------------------------- dynamic_object62={ .@java.lang.Object={ .@class_identifier="java::java.lang.StringBuilder", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 475 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object62.@java.lang.Object.@class_identifier (00001010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 489 file java/lang/StringBuilder.java line 104 function java::java.lang.StringBuilder.:()V thread 0 ---------------------------------------------------- dynamic_object62={ .@java.lang.Object={ .@class_identifier="java::java.lang.StringBuilder", .cproverMonitorCount=0 }, .length=0, .data=nondet_infinite_array!0@4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00001010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 495 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- this=&dynamic_object62.@java.lang.Object.@class_identifier (00001010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 496 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 5 thread 0 ---------------------------------------------------- str=&String_20index_20out_20of_20range_3a_20.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 528 file java/lang/StringBuilder.java line 178 function java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder; thread 0 ---------------------------------------------------- dynamic_object62={ .@java.lang.Object={ .@class_identifier="java::java.lang.StringBuilder", .cproverMonitorCount=0 }, .length=27, .data=nondet_infinite_array$0!0@7 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011011, 00001010 01000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 536 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 7 thread 0 ---------------------------------------------------- this=&dynamic_object62.@java.lang.Object.@class_identifier (00001010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 537 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 7 thread 0 ---------------------------------------------------- i=1 (00000000 00000000 00000000 00000001) State 543 thread 0 ---------------------------------------------------- java$$java_lang_String$$clinit_already_run=true (1) State 548 file java/lang/String.java line 1614 function java::java.lang.String.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object63={ .@class_identifier="java::java.lang.String" } ({ ? }) State 550 file java/lang/String.java line 1614 function java::java.lang.String.:()V bytecode-index 2 thread 0 ---------------------------------------------------- CASE_INSENSITIVE_ORDER=&dynamic_object63.@class_identifier (00001010 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 551 thread 0 ---------------------------------------------------- dynamic_object63={ .@class_identifier="java::java.util.Comparator" } ({ ? }) State 556 file java/lang/StringBuilder.java line 293 function java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder; bytecode-index 2 thread 0 ---------------------------------------------------- i=1 (00000000 00000000 00000000 00000001) State 570 file java/lang/String.java line 3871 function java::java.lang.String.valueOf:(I)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object64={ .@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 574 file java/lang/String.java line 3871 function java::java.lang.String.valueOf:(I)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object64={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=1, .data=nondet_infinite_array$1!0@4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000001, 00001010 10000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 582 file java/lang/StringBuilder.java line 293 function java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder; bytecode-index 3 thread 0 ---------------------------------------------------- this=&dynamic_object62.@java.lang.Object.@class_identifier (00001010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 583 file java/lang/StringBuilder.java line 293 function java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder; bytecode-index 3 thread 0 ---------------------------------------------------- str=&dynamic_object64.@java.lang.Object.@class_identifier (00001010 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 615 file java/lang/StringBuilder.java line 178 function java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder; thread 0 ---------------------------------------------------- dynamic_object62={ .@java.lang.Object={ .@class_identifier="java::java.lang.StringBuilder", .cproverMonitorCount=0 }, .length=28, .data=nondet_infinite_array$0!0@8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011100, 00001010 11000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 627 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 8 thread 0 ---------------------------------------------------- this=&dynamic_object62.@java.lang.Object.@class_identifier (00001010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 638 file java/lang/StringBuilder.java line 631 function java::java.lang.StringBuilder.toString:()Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object68={ .@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 642 file java/lang/StringBuilder.java line 631 function java::java.lang.StringBuilder.toString:()Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object68={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=28, .data=nondet_infinite_array$0!0@8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011100, 00001010 11000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 650 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 651 file java/lang/StringIndexOutOfBoundsException.java line 41 function java::java.lang.StringIndexOutOfBoundsException.:(I)V bytecode-index 9 thread 0 ---------------------------------------------------- s=&dynamic_object68.@java.lang.Object.@class_identifier (00001011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 655 file java/lang/IndexOutOfBoundsException.java line 37 function java::java.lang.IndexOutOfBoundsException.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 656 file java/lang/IndexOutOfBoundsException.java line 37 function java::java.lang.IndexOutOfBoundsException.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- message=&dynamic_object68.@java.lang.Object.@class_identifier (00001011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 660 file java/lang/RuntimeException.java line 36 function java::java.lang.RuntimeException.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 661 file java/lang/RuntimeException.java line 36 function java::java.lang.RuntimeException.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- message=&dynamic_object68.@java.lang.Object.@class_identifier (00001011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 665 file java/lang/Exception.java line 66 function java::java.lang.Exception.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 666 file java/lang/Exception.java line 66 function java::java.lang.Exception.:(Ljava/lang/String;)V bytecode-index 2 thread 0 ---------------------------------------------------- message=&dynamic_object68.@java.lang.Object.@class_identifier (00001011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 670 file java/lang/Throwable.java line 279 function java::java.lang.Throwable.:(Ljava/lang/String;)V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 672 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 676 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:(Ljava/lang/String;)V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.cause=&dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 678 file java/lang/Throwable.java line 281 function java::java.lang.Throwable.:(Ljava/lang/String;)V bytecode-index 7 thread 0 ---------------------------------------------------- dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.detailMessage=&dynamic_object68.@java.lang.Object.@class_identifier (00001011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 700 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- OUTPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 701 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- OUTPUT uncaught_exception': &dynamic_object61.@java.lang.IndexOutOfBoundsException.@java.lang.RuntimeException.@java.lang.Exception.@java.lang.Throwable.@java.lang.Object.@class_identifier (00001001 11100000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V no uncaught exception uncaught_exception' == null VERIFICATION FAILED EC=10 FALSE