./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/StringMiscellaneous04_true-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.MMqgYC.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/StringMiscellaneous04_true-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/StringMiscellaneous04_true-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 2246 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 28 function java::Main.main:([Ljava/lang/String;)V bytecode-index 15 thread 0 aborting path on assume(false) at file Main.java line 29 function java::Main.main:([Ljava/lang/String;)V bytecode-index 25 thread 0 aborting path on assume(false) at file Main.java line 30 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 35 function java::Main.main:([Ljava/lang/String;)V bytecode-index 63 thread 0 aborting path on assume(false) at file Main.java line 38 function java::Main.main:([Ljava/lang/String;)V bytecode-index 76 thread 0 aborting path on assume(false) at file Main.java line 41 function java::Main.main:([Ljava/lang/String;)V bytecode-index 89 thread 0 aborting path on assume(false) at file Main.java line 44 function java::Main.main:([Ljava/lang/String;)V bytecode-index 102 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 1 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 2 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 3 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 4 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 5 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 6 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 7 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 Unwinding loop java::Main.toCharArray:(Ljava/lang/String;)[C.0 iteration 8 file Main.java line 17 function java::Main.toCharArray:(Ljava/lang/String;)[C bytecode-index 31 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 1 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 2 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 3 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 4 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 5 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 6 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 7 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 135 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 8 file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 size of program expression: 2668 steps simple slicing removed 25 assignments Generated 16 VCC(s), 15 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 32017 variables, 28161 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 51437 variables, 86657 clauses SAT checker: instance is UNSATISFIABLE BV-Refinement: got UNSAT, and the proof passes => UNSAT Total iterations: 1 Runtime decision procedure: 0.0906935s VERIFICATION SUCCESSFUL EC=0 TRUE