./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/Class_method1_true-assert.jar


--------------------------------------------------------------------------------


./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.7qmn0G.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/Class_method1_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/Class_method1_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.<init>
 signature: ()V
 descriptor: (Ljava/lang/String;I)V
 different number of parameters, reverting to descriptor
Class: java.lang.Enum
 could not parse signature: <E:Ljava/lang/Enum<TE;>;>Ljava/lang/Object;Ljava/lang/Comparable<TE;>;Ljava/io/Serializable;
 Unsupported class signature: Failed to find generic signature closing delimiter (or recursive generic): java/lang/Enum<TE
 ignoring that the class is generic
Method: java::java.lang.Enum.valueOf
 could not parse signature: <T:Ljava/lang/Enum<TT;>;>(Ljava/lang/Class<TT;>;Ljava/lang/String;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Class;Ljava/lang/String;)Ljava/lang/Enum;
Method: java::org.cprover.CProver.nondetWithNull
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNull
 could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNull
 could not parse signature: <T:Ljava/lang/Object;>(TT;)TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: (Ljava/lang/Object;)Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithNullForNotModelled
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Method: java::org.cprover.CProver.nondetWithoutNullForNotModelled
 could not parse signature: <T:Ljava/lang/Object;>()TT;
 Unsupported class signature: Cannot currently parse bounds on generic types
 reverting to descriptor: ()Ljava/lang/Object;
Java: added 2220 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
size of program expression: 423 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
EC=0
TRUE