./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/StringValueOf02_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.OgYE4G.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/StringValueOf02_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/StringValueOf02_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 2222 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 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 94 thread 0 size of program expression: 11851 steps simple slicing removed 1 assignments Generated 83 VCC(s), 2 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 362759 variables, 904942 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 2.53761s 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 ---------------------------------------------------- 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 5 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 6 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- difffblue_return_value=0 (00000000 00000000 00000000 00000000) State 7 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- difffblue={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=9, .data=difffblue_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001001, 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 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 9 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 11 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 12 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 13 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- difffblue_constarray={ (char)'d', (char)'i', (char)'f', (char)'f', (char)'f', (char)'b', (char)'l', (char)'u', (char)'e' } ({ 00000000 01100100, 00000000 01101001, 00000000 01100110, 00000000 01100110, 00000000 01100110, 00000000 01100010, 00000000 01101100, 00000000 01110101, 00000000 01100101 }) State 14 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 17 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 18 thread 0 ---------------------------------------------------- name=&Main.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 19 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 20 thread 0 ---------------------------------------------------- isArray=false (00000000) State 21 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 22 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 23 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 24 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 25 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 27 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0 ---------------------------------------------------- Main@class_model.name=&Main.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000) State 29 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0 ---------------------------------------------------- Main@class_model.isAnnotation=false (00000000) State 31 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0 ---------------------------------------------------- Main@class_model.isArray=false (00000000) State 33 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0 ---------------------------------------------------- Main@class_model.isInterface=false (00000000) State 35 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0 ---------------------------------------------------- Main@class_model.isSynthetic=false (00000000) State 37 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0 ---------------------------------------------------- Main@class_model.isLocalClass=false (00000000) State 39 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0 ---------------------------------------------------- Main@class_model.isMemberClass=false (00000000) State 41 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0 ---------------------------------------------------- Main@class_model.isEnum=false (00000000) State 43 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 55 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 57 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 58 thread 0 ---------------------------------------------------- dynamic_object1.length=5 (00000000 00000000 00000000 00000101) State 61 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 62 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 67 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 69 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 75 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 79 thread 0 ---------------------------------------------------- dynamic_object4={ (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'?' } ({ 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00111111 }) State 84 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 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 85 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 90 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 92 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 98 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 102 thread 0 ---------------------------------------------------- dynamic_object6={ } ( }) State 107 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 108 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 113 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 115 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 121 thread 0 ---------------------------------------------------- dynamic_object8=dynamic_object8#1 (?) State 125 thread 0 ---------------------------------------------------- dynamic_object8={ } ( }) State 130 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 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 131 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 136 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 138 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 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 144 thread 0 ---------------------------------------------------- dynamic_object10=dynamic_object10#1 (?) State 148 thread 0 ---------------------------------------------------- dynamic_object10={ } ( }) State 153 thread 0 ---------------------------------------------------- dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object10 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 154 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 159 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 161 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 (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 167 thread 0 ---------------------------------------------------- dynamic_object12=dynamic_object12#1 (?) State 171 thread 0 ---------------------------------------------------- dynamic_object12={ } ( }) State 176 thread 0 ---------------------------------------------------- dynamic_object11={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object12 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 177 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 181 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 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 184 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 204 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V bytecode-index 11 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 212 thread 0 ---------------------------------------------------- anonlocal::2a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 213 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 225 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 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 227 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 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 228 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 thread 0 ---------------------------------------------------- dynamic_object17.length=8 (00000000 00000000 00000000 00001000) State 231 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 thread 0 ---------------------------------------------------- dynamic_object17.data=dynamic_18_array (?) State 232 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 16 thread 0 ---------------------------------------------------- dynamic_18_array={ (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000', (char)'\u0000' } ({ 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000, 00000000 00000000 }) State 242 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 23 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 243 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 23 thread 0 ---------------------------------------------------- index=0 (00000000 00000000 00000000 00000000) State 249 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 260 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 261 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 285 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_18_array[0L]=(char)'\u0000' (00000000 00000000) State 295 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 296 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0 ---------------------------------------------------- index=1 (00000000 00000000 00000000 00000001) State 302 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 313 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 314 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=1 (00000000 00000000 00000000 00000001) State 338 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 32 thread 0 ---------------------------------------------------- dynamic_18_array[1L]=(char)'\u0000' (00000000 00000000) State 348 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 39 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 349 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 39 thread 0 ---------------------------------------------------- index=2 (00000000 00000000 00000000 00000010) State 355 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 (00000001 00000000 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_object3.@java.lang.Object.@class_identifier (00000001 00000000 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=2 (00000000 00000000 00000000 00000010) State 391 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 40 thread 0 ---------------------------------------------------- dynamic_18_array[2L]=(char)'\u0000' (00000000 00000000) State 401 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 47 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 402 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 47 thread 0 ---------------------------------------------------- index=3 (00000000 00000000 00000000 00000011) State 408 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 419 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 (00000001 00000000 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 ---------------------------------------------------- i=3 (00000000 00000000 00000000 00000011) State 444 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 48 thread 0 ---------------------------------------------------- dynamic_18_array[3L]=(char)'\u0000' (00000000 00000000) State 454 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 55 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 455 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 55 thread 0 ---------------------------------------------------- index=4 (00000000 00000000 00000000 00000100) State 461 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 472 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 473 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=4 (00000000 00000000 00000000 00000100) State 497 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 56 thread 0 ---------------------------------------------------- dynamic_18_array[4L]=(char)'\u0000' (00000000 00000000) State 507 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 63 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 508 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 63 thread 0 ---------------------------------------------------- index=5 (00000000 00000000 00000000 00000101) State 514 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 525 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 526 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=5 (00000000 00000000 00000000 00000101) State 550 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 64 thread 0 ---------------------------------------------------- dynamic_18_array[5L]=(char)'\u0000' (00000000 00000000) State 560 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 71 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 561 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 71 thread 0 ---------------------------------------------------- index=6 (00000000 00000000 00000000 00000110) State 567 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 578 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 579 file java/lang/String.java line 771 function java::java.lang.String.charAt:(I)C bytecode-index 13 thread 0 ---------------------------------------------------- i=6 (00000000 00000000 00000000 00000110) State 603 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 72 thread 0 ---------------------------------------------------- dynamic_18_array[6L]=(char)'\u0000' (00000000 00000000) State 613 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 79 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 614 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 79 thread 0 ---------------------------------------------------- index=7 (00000000 00000000 00000000 00000111) State 620 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 631 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 (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 632 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 656 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 80 thread 0 ---------------------------------------------------- dynamic_18_array[7L]=(char)'\u0000' (00000000 00000000) State 657 file Main.java line 15 function java::Main.main:([Ljava/lang/String;)V bytecode-index 81 thread 0 ---------------------------------------------------- anonlocal::1a=&dynamic_object17.@java.lang.Object.@class_identifier (00000010 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 661 thread 0 ---------------------------------------------------- java$$java_lang_String$$clinit_already_run=true (1) State 666 file java/lang/String.java line 1614 function java::java.lang.String.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object128={ .@class_identifier="java::java.lang.String" } ({ ? }) State 668 file java/lang/String.java line 1614 function java::java.lang.String.:()V bytecode-index 2 thread 0 ---------------------------------------------------- CASE_INSENSITIVE_ORDER=&dynamic_object128.@class_identifier (00010100 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 669 thread 0 ---------------------------------------------------- dynamic_object128={ .@class_identifier="java::java.util.Comparator" } ({ ? }) State 674 file Main.java line 16 function java::Main.main:([Ljava/lang/String;)V bytecode-index 83 thread 0 ---------------------------------------------------- data=&dynamic_object17.@java.lang.Object.@class_identifier (00000010 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 680 file java/lang/String.java line 3753 function java::java.lang.String.valueOf:([C)Ljava/lang/String; bytecode-index 3 thread 0 ---------------------------------------------------- dynamic_object129={ .@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 688 thread 0 ---------------------------------------------------- dynamic_object130=dynamic_object130#1 (?) State 692 thread 0 ---------------------------------------------------- dynamic_object130={ } ( }) State 697 thread 0 ---------------------------------------------------- dynamic_object129={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=0, .data=dynamic_object130 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00010101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 698 file java/lang/String.java line 3753 function java::java.lang.String.valueOf:([C)Ljava/lang/String; bytecode-index 3 thread 0 ---------------------------------------------------- dynamic_object129.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 701 file Main.java line 16 function java::Main.main:([Ljava/lang/String;)V bytecode-index 84 thread 0 ---------------------------------------------------- anonlocal::2a=&dynamic_object129.@java.lang.Object.@class_identifier (00010101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 705 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 713 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 714 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 719 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 720 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 725 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 729 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 736 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 741 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 758 file Main.java line 8 function java::Main.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 768 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 89 thread 0 ---------------------------------------------------- this=&dynamic_object129.@java.lang.Object.@class_identifier (00010101 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 769 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 89 thread 0 ---------------------------------------------------- anObject=&difffblue.@java.lang.Object.@class_identifier (00010101 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 799 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 91 thread 0 ---------------------------------------------------- dynamic_object131={ .@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 801 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 91 thread 0 ---------------------------------------------------- dynamic_object131={ .@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 805 file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 93 thread 0 ---------------------------------------------------- this=&dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00010101 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 809 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00010101 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 813 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00010101 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 817 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00010101 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 819 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 823 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object131.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object131.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00010101 01100000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 94 assertion at file Main.java line 17 function java::Main.main:([Ljava/lang/String;)V bytecode-index 94 false VERIFICATION FAILED EC=10 FALSE