./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/aastore_aaload1_true-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.50OZTn.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/aastore_aaload1_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/aastore_aaload1_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 2219 String or Class constant symbols Generating GOTO Program Running GOTO functions transformation passes Running with 11 object bits, 53 offset bits (user-specified) Starting Bounded Model Checking Unwinding loop __CPROVER__start.0 iteration 1 thread 0 Unwinding loop __CPROVER__start.0 iteration 2 thread 0 Unwinding loop __CPROVER__start.0 iteration 3 thread 0 Unwinding loop __CPROVER__start.0 iteration 4 thread 0 Unwinding loop __CPROVER__start.0 iteration 5 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 1 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 2 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 3 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 4 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 5 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 6 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 7 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 8 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 9 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 10 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Not unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 11 file Main.java line 18 function java::Main.main:([Ljava/lang/String;)V bytecode-index 18 thread 0 Unwinding recursion java::Main::clinit_wrapper iteration 1 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 1 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 2 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 3 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 4 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 5 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 6 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 7 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 8 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 9 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 10 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 aborting path on assume(false) at file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 33 thread 0 Not unwinding loop java::Main.main:([Ljava/lang/String;)V.1 iteration 11 file Main.java line 21 function java::Main.main:([Ljava/lang/String;)V bytecode-index 35 thread 0 size of program expression: 3571 steps simple slicing removed 1 assignments Generated 35 VCC(s), 12 remaining after simplification Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier converting SSA Running string refinement loop with MiniSAT 2.2.1 without simplifier BV-Refinement: post-processing BV-Refinement: iteration 1 441299 variables, 1225981 clauses SAT checker: instance is UNSATISFIABLE BV-Refinement: got UNSAT, and the proof passes => UNSAT Total iterations: 1 Runtime decision procedure: 0.622864s VERIFICATION SUCCESSFUL EC=0 TRUE