./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/StringConcatenation03_false-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.rlkHqi.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/StringConcatenation03_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/StringConcatenation03_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 2231 String or Class constant symbols Generating GOTO Program Running GOTO functions transformation passes Running with 11 object bits, 53 offset bits (user-specified) Starting Bounded Model Checking Unwinding loop __CPROVER__start.0 iteration 1 thread 0 Unwinding loop __CPROVER__start.0 iteration 2 thread 0 Unwinding loop __CPROVER__start.0 iteration 3 thread 0 Unwinding loop __CPROVER__start.0 iteration 4 thread 0 Unwinding loop __CPROVER__start.0 iteration 5 thread 0 Unwinding recursion java::Main::clinit_wrapper iteration 1 aborting path on assume(false) at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 46 thread 0 aborting path on assume(false) at file Main.java line 25 function java::Main.main:([Ljava/lang/String;)V bytecode-index 68 thread 0 size of program expression: 2538 steps simple slicing removed 1 assignments Generated 23 VCC(s), 3 remaining after simplification Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier converting SSA Running string refinement loop with MiniSAT 2.2.1 without simplifier BV-Refinement: post-processing BV-Refinement: iteration 1 65533 variables, 108347 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 BV-Refinement: post-processing BV-Refinement: iteration 1 93908 variables, 226106 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 BV-Refinement: post-processing BV-Refinement: iteration 1 234832 variables, 879755 clauses SAT checker: instance is SATISFIABLE BV-Refinement: got SAT, and it simulates => SAT Total iterations: 1 Runtime decision procedure: 1.16379s 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 ---------------------------------------------------- s1_20after_20concatenation_20_3d_20_25s_0a_return_value=0 (00000000 00000000 00000000 00000000) State 5 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at_20DiffBllue_return_value=0 (00000000 00000000 00000000 00000000) State 6 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 9 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 10 thread 0 ---------------------------------------------------- name=&Main.@java.lang.Object.@class_identifier (00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 11 thread 0 ---------------------------------------------------- isAnnotation=false (00000000) State 12 thread 0 ---------------------------------------------------- isArray=false (00000000) State 13 thread 0 ---------------------------------------------------- isInterface=false (00000000) State 14 thread 0 ---------------------------------------------------- isSynthetic=false (00000000) State 15 thread 0 ---------------------------------------------------- isLocalClass=false (00000000) State 16 thread 0 ---------------------------------------------------- isMemberClass=false (00000000) State 17 thread 0 ---------------------------------------------------- isEnum=false (00000000) State 19 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 01100000 00000000 00000000 00000000 00000000 00000000 00000000) State 21 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 23 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 25 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 27 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 29 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 31 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 33 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 36 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at_20DiffBllue={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=18, .data=Happy_20at_20DiffBllue_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00010010, 00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 37 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=8, .data=Happy_20at_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001000, 00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 38 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at_return_value=0 (00000000 00000000 00000000 00000000) State 39 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- out=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 40 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- s1_20after_20concatenation_20_3d_20_25s_0a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=28, .data=s1_20after_20concatenation_20_3d_20_25s_0a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011100, 00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 42 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$java_lang_System$$clinit_already_run=false (0) State 43 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Result_20of_20s1_2econcat_28s2_29_20_3d_20_25s_0a_constarray={ (char)'R', (char)'e', (char)'s', (char)'u', (char)'l', (char)'t', (char)' ', (char)'o', (char)'f', (char)' ', (char)'s', (char)'1', (char)'.', (char)'c', (char)'o', (char)'n', (char)'c', (char)'a', (char)'t', (char)'(', (char)'s', (char)'2', (char)')', (char)' ', (char)'=', (char)' ', (char)'%', (char)'s', (char)'\n' } ({ 00000000 01010010, 00000000 01100101, 00000000 01110011, 00000000 01110101, 00000000 01101100, 00000000 01110100, 00000000 00100000, 00000000 01101111, 00000000 01100110, 00000000 00100000, 00000000 01110011, 00000000 00110001, 00000000 00101110, 00000000 01100011, 00000000 01101111, 00000000 01101110, 00000000 01100011, 00000000 01100001, 00000000 01110100, 00000000 00101000, 00000000 01110011, 00000000 00110010, 00000000 00101001, 00000000 00100000, 00000000 00111101, 00000000 00100000, 00000000 00100101, 00000000 01110011, 00000000 00001010 }) State 44 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at_constarray={ (char)'H', (char)'a', (char)'p', (char)'p', (char)'y', (char)' ', (char)'a', (char)'t' } ({ 00000000 01001000, 00000000 01100001, 00000000 01110000, 00000000 01110000, 00000000 01111001, 00000000 00100000, 00000000 01100001, 00000000 01110100 }) State 45 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Result_20of_20s1_2econcat_28s2_29_20_3d_20_25s_0a={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=29, .data=Result_20of_20s1_2econcat_28s2_29_20_3d_20_25s_0a_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00011101, 00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 46 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=false (0) State 47 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Happy_20at_20DiffBllue_constarray={ (char)'H', (char)'a', (char)'p', (char)'p', (char)'y', (char)' ', (char)'a', (char)'t', (char)' ', (char)'D', (char)'i', (char)'f', (char)'f', (char)'B', (char)'l', (char)'l', (char)'u', (char)'e' } ({ 00000000 01001000, 00000000 01100001, 00000000 01110000, 00000000 01110000, 00000000 01111001, 00000000 00100000, 00000000 01100001, 00000000 01110100, 00000000 00100000, 00000000 01000100, 00000000 01101001, 00000000 01100110, 00000000 01100110, 00000000 01000010, 00000000 01101100, 00000000 01101100, 00000000 01110101, 00000000 01100101 }) State 48 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 49 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- Result_20of_20s1_2econcat_28s2_29_20_3d_20_25s_0a_return_value=0 (00000000 00000000 00000000 00000000) State 50 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- s1_20after_20concatenation_20_3d_20_25s_0a_constarray={ (char)'s', (char)'1', (char)' ', (char)'a', (char)'f', (char)'t', (char)'e', (char)'r', (char)' ', (char)'c', (char)'o', (char)'n', (char)'c', (char)'a', (char)'t', (char)'e', (char)'n', (char)'a', (char)'t', (char)'i', (char)'o', (char)'n', (char)' ', (char)'=', (char)' ', (char)'%', (char)'s', (char)'\n' } ({ 00000000 01110011, 00000000 00110001, 00000000 00100000, 00000000 01100001, 00000000 01100110, 00000000 01110100, 00000000 01100101, 00000000 01110010, 00000000 00100000, 00000000 01100011, 00000000 01101111, 00000000 01101110, 00000000 01100011, 00000000 01100001, 00000000 01110100, 00000000 01100101, 00000000 01101110, 00000000 01100001, 00000000 01110100, 00000000 01101001, 00000000 01101111, 00000000 01101110, 00000000 00100000, 00000000 00111101, 00000000 00100000, 00000000 00100101, 00000000 01110011, 00000000 00001010 }) State 62 thread 0 ---------------------------------------------------- dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 64 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 65 thread 0 ---------------------------------------------------- dynamic_object1.length=5 (00000000 00000000 00000000 00000101) State 68 thread 0 ---------------------------------------------------- dynamic_object1.data=dynamic_2_array (00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 69 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 74 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.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 76 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 82 thread 0 ---------------------------------------------------- dynamic_object4=dynamic_object4#1 (?) State 86 thread 0 ---------------------------------------------------- dynamic_object4={ (char)'`', (char)'`', (char)'`', (char)'\u0161', (char)'`', (char)' ', (char)'`', (char)'\u0161', (char)'`', (char)'\u8160', (char)'p', (char)'`', (char)'\u6040', (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)'`', (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)'`', (char)'`', (char)'`', (char)'`', (char)'`', (char)'`', (char)'`', (char)'`', (char)'`', (char)'`' } ({ 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000001 01100001, 00000000 01100000, 00000000 00100000, 00000000 01100000, 00000001 01100001, 00000000 01100000, 10000001 01100000, 00000000 01110000, 00000000 01100000, 01100000 01000000, 00000000 01000000, 00000000 01100000, 00000000 01000000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000, 00000000 01100000 }) State 91 thread 0 ---------------------------------------------------- dynamic_object3={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=76, .data=dynamic_object4 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 01001100, 00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 92 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 97 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.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 99 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 105 thread 0 ---------------------------------------------------- dynamic_object6=dynamic_object6#1 (?) State 109 thread 0 ---------------------------------------------------- dynamic_object6={ (char)'\ufacb', (char)'\ufa80', (char)'\uffc8', (char)'\ufa88', (char)'\uff88', (char)'\u7f99', (char)'\ufac9', (char)'\ufadc' } ({ 11111010 11001011, 11111010 10000000, 11111111 11001000, 11111010 10001000, 11111111 10001000, 01111111 10011001, 11111010 11001001, 11111010 11011100 }) State 114 thread 0 ---------------------------------------------------- dynamic_object5={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=8, .data=dynamic_object6 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001000, 00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 115 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 120 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.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 122 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 11000000 00000000 00000000 00000000 00000000 00000000 00000000) State 128 thread 0 ---------------------------------------------------- dynamic_object8=dynamic_object8#1 (?) State 132 thread 0 ---------------------------------------------------- dynamic_object8={ (char)'\u80cc', (char)'\u80cf', (char)'\u80c9', (char)'\u80cc', (char)'\u80cc', (char)'\u00c6', (char)'\u80cc', (char)'\u805d' } ({ 10000000 11001100, 10000000 11001111, 10000000 11001001, 10000000 11001100, 10000000 11001100, 00000000 11000110, 10000000 11001100, 10000000 01011101 }) State 137 thread 0 ---------------------------------------------------- dynamic_object7={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=8, .data=dynamic_object8 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001000, 00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 138 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 143 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.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 145 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- dynamic_2_array[3L]=&dynamic_object9.@java.lang.Object.@class_identifier (00000010 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 151 thread 0 ---------------------------------------------------- dynamic_object10=dynamic_object10#1 (?) State 155 thread 0 ---------------------------------------------------- dynamic_object10={ (char)'\uf462', (char)'\uf461', (char)'\uf063', (char)'\uf467', (char)'\uf462', (char)'\u7532', (char)'\uf462', (char)'\ufc63' } ({ 11110100 01100010, 11110100 01100001, 11110000 01100011, 11110100 01100111, 11110100 01100010, 01110101 00110010, 11110100 01100010, 11111100 01100011 }) State 160 thread 0 ---------------------------------------------------- dynamic_object9={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=8, .data=dynamic_object10 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001000, 00000010 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 161 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 166 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.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 168 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 174 thread 0 ---------------------------------------------------- dynamic_object12=dynamic_object12#1 (?) State 178 thread 0 ---------------------------------------------------- dynamic_object12={ (char)'\ua19d', (char)'\ua19d', (char)'\ua19d', (char)'\ua19d', (char)'\ua19d', (char)'\ua199', (char)'\ua19d', (char)'\ua19d' } ({ 10100001 10011101, 10100001 10011101, 10100001 10011101, 10100001 10011101, 10100001 10011101, 10100001 10011001, 10100001 10011101, 10100001 10011101 }) State 183 thread 0 ---------------------------------------------------- dynamic_object11={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=8, .data=dynamic_object12 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00001000, 00000010 01100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 184 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 188 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 191 file Main.java line 12 function java::Main.main:([Ljava/lang/String;)V thread 0 ---------------------------------------------------- arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 208 thread 0 ---------------------------------------------------- anonlocal::3a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 209 thread 0 ---------------------------------------------------- anonlocal::1a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 210 thread 0 ---------------------------------------------------- anonlocal::2a=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 221 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 (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 228 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 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 232 thread 0 ---------------------------------------------------- java$$java_lang_System$$clinit_already_run=true (1) State 236 thread 0 ---------------------------------------------------- dynamic_object17={ .@class_identifier="java::java.lang.Class" } ({ ? }) State 238 thread 0 ---------------------------------------------------- out=&dynamic_object17.@class_identifier (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 239 thread 0 ---------------------------------------------------- dynamic_object17={ .@class_identifier="java::java.io.PrintStream" } ({ ? }) State 243 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 245 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_object18={ .@java.lang.Object={ .@class_identifier="java::array[reference]", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 246 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_object18.length=1 (00000000 00000000 00000000 00000001) State 249 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_object18.data=dynamic_19_array (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 250 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 24 thread 0 ---------------------------------------------------- dynamic_19_array={ null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 254 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 29 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 255 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 29 thread 0 ---------------------------------------------------- str=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 287 file java/lang/String.java line 2594 function java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 291 file java/lang/String.java line 2594 function java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object25={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=84, .data=nondet_infinite_array!0@1 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 01010100, 00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 302 file Main.java line 19 function java::Main.main:([Ljava/lang/String;)V bytecode-index 30 thread 0 ---------------------------------------------------- dynamic_19_array[0L]=&dynamic_object25.@java.lang.Object.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 306 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0 ---------------------------------------------------- this=&dynamic_object17.@class_identifier (00000011 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 307 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0 ---------------------------------------------------- stub_ignored_arg1=&Result_20of_20s1_2econcat_28s2_29_20_3d_20_25s_0a.@java.lang.Object.@class_identifier (00000100 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 308 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 31 thread 0 ---------------------------------------------------- stub_ignored_arg2=&dynamic_object18.@java.lang.Object.@class_identifier (00000011 00100000 00000000 00000000 00000000 00000000 00000000 00000000) State 319 file Main.java line 20 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 ---------------------------------------------------- this=&dynamic_object3.@java.lang.Object.@class_identifier (00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 320 file Main.java line 20 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 ---------------------------------------------------- str=&dynamic_object5.@java.lang.Object.@class_identifier (00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 352 file java/lang/String.java line 2594 function java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 356 file java/lang/String.java line 2594 function java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String; thread 0 ---------------------------------------------------- dynamic_object32={ .@java.lang.Object={ .@class_identifier="java::java.lang.String", .cproverMonitorCount=0 }, .length=84, .data=nondet_infinite_array!0@2 } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 01010100, 00000101 00100000 00000000 00000000 00000000 00000000 00000000 00000000 }) State 361 file Main.java line 20 function java::Main.main:([Ljava/lang/String;)V bytecode-index 36 thread 0 ---------------------------------------------------- anonlocal::3a=&dynamic_object32.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 365 thread 0 ---------------------------------------------------- java$$Main$$clinit_already_run=true (1) State 373 file Main.java line 8 function java::Main.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 374 thread 0 ---------------------------------------------------- loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 379 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 380 thread 0 ---------------------------------------------------- cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000) State 385 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 389 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 396 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 401 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 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 418 file Main.java line 8 function java::Main.:()V bytecode-index 6 thread 0 ---------------------------------------------------- $assertionsDisabled=false (00000000) State 428 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 41 thread 0 ---------------------------------------------------- this=&dynamic_object32.@java.lang.Object.@class_identifier (00000101 01000000 00000000 00000000 00000000 00000000 00000000 00000000) State 429 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 41 thread 0 ---------------------------------------------------- anObject=&Happy_20at_20DiffBllue.@java.lang.Object.@class_identifier (00000101 10000000 00000000 00000000 00000000 00000000 00000000 00000000) State 459 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 43 thread 0 ---------------------------------------------------- dynamic_object36={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class", .cproverMonitorCount=0 }, .detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } }) State 461 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 43 thread 0 ---------------------------------------------------- dynamic_object36={ .@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 465 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 45 thread 0 ---------------------------------------------------- this=&dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 469 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 473 file java/lang/Error.java line 58 function java::java.lang.Error.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 477 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.:()V bytecode-index 1 thread 0 ---------------------------------------------------- this=&dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) State 479 file java/lang/Object.java line 40 function java::java.lang.Object.:()V bytecode-index 2 thread 0 ---------------------------------------------------- dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000) State 483 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.:()V bytecode-index 4 thread 0 ---------------------------------------------------- dynamic_object36.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object36.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000101 11100000 00000000 00000000 00000000 00000000 00000000 00000000) Violated property: file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 46 assertion at file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 46 false VERIFICATION FAILED EC=10 FALSE