./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jbmc-regression/astore_aload1_true-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.GPXo8U.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jbmc-regression/astore_aload1_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/astore_aload1_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 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 2 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 3 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 4 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 5 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 6 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 7 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 8 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 9 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding loop java::Main.main:([Ljava/lang/String;)V.0 iteration 10 file Main.java line 22 function java::Main.main:([Ljava/lang/String;)V bytecode-index 78 thread 0 Unwinding recursion java::Main::clinit_wrapper iteration 1 aborting path on assume(false) at file Main.java line 38 function java::Main.main:([Ljava/lang/String;)V bytecode-index 98 thread 0 aborting path on assume(false) at file Main.java line 39 function java::Main.main:([Ljava/lang/String;)V bytecode-index 108 thread 0 aborting path on assume(false) at file Main.java line 40 function java::Main.main:([Ljava/lang/String;)V bytecode-index 118 thread 0 aborting path on assume(false) at file Main.java line 41 function java::Main.main:([Ljava/lang/String;)V bytecode-index 128 thread 0 aborting path on assume(false) at file Main.java line 42 function java::Main.main:([Ljava/lang/String;)V bytecode-index 138 thread 0 aborting path on assume(false) at file Main.java line 43 function java::Main.main:([Ljava/lang/String;)V bytecode-index 148 thread 0 aborting path on assume(false) at file Main.java line 44 function java::Main.main:([Ljava/lang/String;)V bytecode-index 158 thread 0 aborting path on assume(false) at file Main.java line 45 function java::Main.main:([Ljava/lang/String;)V bytecode-index 168 thread 0 aborting path on assume(false) at file Main.java line 46 function java::Main.main:([Ljava/lang/String;)V bytecode-index 178 thread 0 aborting path on assume(false) at file Main.java line 47 function java::Main.main:([Ljava/lang/String;)V bytecode-index 188 thread 0 aborting path on assume(false) at file Main.java line 49 function java::Main.main:([Ljava/lang/String;)V bytecode-index 208 thread 0 aborting path on assume(false) at file Main.java line 50 function java::Main.main:([Ljava/lang/String;)V bytecode-index 219 thread 0 aborting path on assume(false) at file Main.java line 51 function java::Main.main:([Ljava/lang/String;)V bytecode-index 230 thread 0 aborting path on assume(false) at file Main.java line 52 function java::Main.main:([Ljava/lang/String;)V bytecode-index 241 thread 0 aborting path on assume(false) at file Main.java line 53 function java::Main.main:([Ljava/lang/String;)V bytecode-index 252 thread 0 aborting path on assume(false) at file Main.java line 54 function java::Main.main:([Ljava/lang/String;)V bytecode-index 263 thread 0 aborting path on assume(false) at file Main.java line 55 function java::Main.main:([Ljava/lang/String;)V bytecode-index 274 thread 0 aborting path on assume(false) at file Main.java line 56 function java::Main.main:([Ljava/lang/String;)V bytecode-index 285 thread 0 aborting path on assume(false) at file Main.java line 57 function java::Main.main:([Ljava/lang/String;)V bytecode-index 296 thread 0 aborting path on assume(false) at file Main.java line 58 function java::Main.main:([Ljava/lang/String;)V bytecode-index 307 thread 0 aborting path on assume(false) at file Main.java line 60 function java::Main.main:([Ljava/lang/String;)V bytecode-index 327 thread 0 aborting path on assume(false) at file Main.java line 61 function java::Main.main:([Ljava/lang/String;)V bytecode-index 338 thread 0 aborting path on assume(false) at file Main.java line 62 function java::Main.main:([Ljava/lang/String;)V bytecode-index 349 thread 0 aborting path on assume(false) at file Main.java line 63 function java::Main.main:([Ljava/lang/String;)V bytecode-index 360 thread 0 aborting path on assume(false) at file Main.java line 64 function java::Main.main:([Ljava/lang/String;)V bytecode-index 371 thread 0 aborting path on assume(false) at file Main.java line 65 function java::Main.main:([Ljava/lang/String;)V bytecode-index 382 thread 0 aborting path on assume(false) at file Main.java line 66 function java::Main.main:([Ljava/lang/String;)V bytecode-index 393 thread 0 aborting path on assume(false) at file Main.java line 67 function java::Main.main:([Ljava/lang/String;)V bytecode-index 404 thread 0 aborting path on assume(false) at file Main.java line 68 function java::Main.main:([Ljava/lang/String;)V bytecode-index 415 thread 0 aborting path on assume(false) at file Main.java line 69 function java::Main.main:([Ljava/lang/String;)V bytecode-index 426 thread 0 aborting path on assume(false) at file Main.java line 71 function java::Main.main:([Ljava/lang/String;)V bytecode-index 446 thread 0 aborting path on assume(false) at file Main.java line 72 function java::Main.main:([Ljava/lang/String;)V bytecode-index 457 thread 0 aborting path on assume(false) at file Main.java line 73 function java::Main.main:([Ljava/lang/String;)V bytecode-index 468 thread 0 aborting path on assume(false) at file Main.java line 74 function java::Main.main:([Ljava/lang/String;)V bytecode-index 479 thread 0 aborting path on assume(false) at file Main.java line 75 function java::Main.main:([Ljava/lang/String;)V bytecode-index 490 thread 0 aborting path on assume(false) at file Main.java line 76 function java::Main.main:([Ljava/lang/String;)V bytecode-index 501 thread 0 aborting path on assume(false) at file Main.java line 77 function java::Main.main:([Ljava/lang/String;)V bytecode-index 512 thread 0 aborting path on assume(false) at file Main.java line 78 function java::Main.main:([Ljava/lang/String;)V bytecode-index 523 thread 0 aborting path on assume(false) at file Main.java line 79 function java::Main.main:([Ljava/lang/String;)V bytecode-index 534 thread 0 aborting path on assume(false) at file Main.java line 80 function java::Main.main:([Ljava/lang/String;)V bytecode-index 545 thread 0 aborting path on assume(false) at file Main.java line 82 function java::Main.main:([Ljava/lang/String;)V bytecode-index 567 thread 0 aborting path on assume(false) at file Main.java line 83 function java::Main.main:([Ljava/lang/String;)V bytecode-index 579 thread 0 aborting path on assume(false) at file Main.java line 84 function java::Main.main:([Ljava/lang/String;)V bytecode-index 591 thread 0 aborting path on assume(false) at file Main.java line 85 function java::Main.main:([Ljava/lang/String;)V bytecode-index 603 thread 0 aborting path on assume(false) at file Main.java line 86 function java::Main.main:([Ljava/lang/String;)V bytecode-index 615 thread 0 aborting path on assume(false) at file Main.java line 87 function java::Main.main:([Ljava/lang/String;)V bytecode-index 627 thread 0 aborting path on assume(false) at file Main.java line 88 function java::Main.main:([Ljava/lang/String;)V bytecode-index 639 thread 0 aborting path on assume(false) at file Main.java line 89 function java::Main.main:([Ljava/lang/String;)V bytecode-index 651 thread 0 aborting path on assume(false) at file Main.java line 90 function java::Main.main:([Ljava/lang/String;)V bytecode-index 663 thread 0 aborting path on assume(false) at file Main.java line 91 function java::Main.main:([Ljava/lang/String;)V bytecode-index 675 thread 0 aborting path on assume(false) at file Main.java line 93 function java::Main.main:([Ljava/lang/String;)V bytecode-index 695 thread 0 aborting path on assume(false) at file Main.java line 94 function java::Main.main:([Ljava/lang/String;)V bytecode-index 706 thread 0 aborting path on assume(false) at file Main.java line 95 function java::Main.main:([Ljava/lang/String;)V bytecode-index 717 thread 0 aborting path on assume(false) at file Main.java line 96 function java::Main.main:([Ljava/lang/String;)V bytecode-index 728 thread 0 aborting path on assume(false) at file Main.java line 97 function java::Main.main:([Ljava/lang/String;)V bytecode-index 739 thread 0 aborting path on assume(false) at file Main.java line 98 function java::Main.main:([Ljava/lang/String;)V bytecode-index 750 thread 0 aborting path on assume(false) at file Main.java line 99 function java::Main.main:([Ljava/lang/String;)V bytecode-index 761 thread 0 aborting path on assume(false) at file Main.java line 100 function java::Main.main:([Ljava/lang/String;)V bytecode-index 772 thread 0 aborting path on assume(false) at file Main.java line 101 function java::Main.main:([Ljava/lang/String;)V bytecode-index 783 thread 0 aborting path on assume(false) at file Main.java line 102 function java::Main.main:([Ljava/lang/String;)V bytecode-index 794 thread 0 aborting path on assume(false) at file Main.java line 104 function java::Main.main:([Ljava/lang/String;)V bytecode-index 815 thread 0 aborting path on assume(false) at file Main.java line 105 function java::Main.main:([Ljava/lang/String;)V bytecode-index 827 thread 0 aborting path on assume(false) at file Main.java line 106 function java::Main.main:([Ljava/lang/String;)V bytecode-index 839 thread 0 aborting path on assume(false) at file Main.java line 107 function java::Main.main:([Ljava/lang/String;)V bytecode-index 851 thread 0 aborting path on assume(false) at file Main.java line 108 function java::Main.main:([Ljava/lang/String;)V bytecode-index 863 thread 0 aborting path on assume(false) at file Main.java line 109 function java::Main.main:([Ljava/lang/String;)V bytecode-index 875 thread 0 aborting path on assume(false) at file Main.java line 110 function java::Main.main:([Ljava/lang/String;)V bytecode-index 887 thread 0 aborting path on assume(false) at file Main.java line 111 function java::Main.main:([Ljava/lang/String;)V bytecode-index 899 thread 0 aborting path on assume(false) at file Main.java line 112 function java::Main.main:([Ljava/lang/String;)V bytecode-index 911 thread 0 aborting path on assume(false) at file Main.java line 113 function java::Main.main:([Ljava/lang/String;)V bytecode-index 923 thread 0 size of program expression: 5228 steps simple slicing removed 11 assignments Generated 71 VCC(s), 70 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 51312 variables, 46902 clauses SAT checker inconsistent: instance is UNSATISFIABLE BV-Refinement: got UNSAT, and the proof passes => UNSAT Total iterations: 1 Runtime decision procedure: 0.0748958s VERIFICATION SUCCESSFUL EC=0 TRUE