./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_true-assert.jar -------------------------------------------------------------------------------- ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.RA6PSY.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_true-assert.jar ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.RA6PSY.witness --unwind 40 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_true-assert.jar ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.RA6PSY.witness --unwind 101 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_true-assert.jar ./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.RA6PSY.witness --unwind 1025 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_true-assert.jar Unwind: 101 JBMC version 5.9 (cbmc-5.7-5176-g7c4b5aa) 64-bit x86_64 linux Parsing ../git-sv-benchmarks/java/jayhorn-recursive/SatEvenOdd01_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' failed to load class `java.util.stream.DoubleStream' failed to load class `java.util.stream.LongStream' 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 recursion java::Main::clinit_wrapper iteration 1 Unwinding recursion Main.isOdd(int) iteration 1 Unwinding recursion Main.isEven(int) iteration 1 Unwinding recursion Main.isOdd(int) iteration 2 Unwinding recursion Main.isEven(int) iteration 2 Unwinding recursion Main.isOdd(int) iteration 3 Unwinding recursion Main.isEven(int) iteration 3 Unwinding recursion Main.isOdd(int) iteration 4 Unwinding recursion Main.isEven(int) iteration 4 Unwinding recursion Main.isOdd(int) iteration 5 Unwinding recursion Main.isEven(int) iteration 5 Unwinding recursion Main.isOdd(int) iteration 6 Unwinding recursion Main.isEven(int) iteration 6 Unwinding recursion Main.isOdd(int) iteration 7 Unwinding recursion Main.isEven(int) iteration 7 Unwinding recursion Main.isOdd(int) iteration 8 Unwinding recursion Main.isEven(int) iteration 8 Unwinding recursion Main.isOdd(int) iteration 9 Unwinding recursion Main.isEven(int) iteration 9 Unwinding recursion Main.isOdd(int) iteration 10 Unwinding recursion Main.isEven(int) iteration 10 Unwinding recursion Main.isOdd(int) iteration 11 Unwinding recursion Main.isEven(int) iteration 11 Unwinding recursion Main.isOdd(int) iteration 12 Unwinding recursion Main.isEven(int) iteration 12 Unwinding recursion Main.isOdd(int) iteration 13 Unwinding recursion Main.isEven(int) iteration 13 Unwinding recursion Main.isOdd(int) iteration 14 Unwinding recursion Main.isEven(int) iteration 14 Unwinding recursion Main.isOdd(int) iteration 15 Unwinding recursion Main.isEven(int) iteration 15 Unwinding recursion Main.isOdd(int) iteration 16 Unwinding recursion Main.isEven(int) iteration 16 Unwinding recursion Main.isOdd(int) iteration 17 Unwinding recursion Main.isEven(int) iteration 17 Unwinding recursion Main.isOdd(int) iteration 18 Unwinding recursion Main.isEven(int) iteration 18 Unwinding recursion Main.isOdd(int) iteration 19 Unwinding recursion Main.isEven(int) iteration 19 Unwinding recursion Main.isOdd(int) iteration 20 Unwinding recursion Main.isEven(int) iteration 20 Unwinding recursion Main.isOdd(int) iteration 21 Unwinding recursion Main.isEven(int) iteration 21 Unwinding recursion Main.isOdd(int) iteration 22 Unwinding recursion Main.isEven(int) iteration 22 Unwinding recursion Main.isOdd(int) iteration 23 Unwinding recursion Main.isEven(int) iteration 23 Unwinding recursion Main.isOdd(int) iteration 24 Unwinding recursion Main.isEven(int) iteration 24 Unwinding recursion Main.isOdd(int) iteration 25 Unwinding recursion Main.isEven(int) iteration 25 Unwinding recursion Main.isOdd(int) iteration 26 Unwinding recursion Main.isEven(int) iteration 26 Unwinding recursion Main.isOdd(int) iteration 27 Unwinding recursion Main.isEven(int) iteration 27 Unwinding recursion Main.isOdd(int) iteration 28 Unwinding recursion Main.isEven(int) iteration 28 Unwinding recursion Main.isOdd(int) iteration 29 Unwinding recursion Main.isEven(int) iteration 29 Unwinding recursion Main.isOdd(int) iteration 30 Unwinding recursion Main.isEven(int) iteration 30 Unwinding recursion Main.isOdd(int) iteration 31 Unwinding recursion Main.isEven(int) iteration 31 Unwinding recursion Main.isOdd(int) iteration 32 Unwinding recursion Main.isEven(int) iteration 32 Unwinding recursion Main.isOdd(int) iteration 33 Unwinding recursion Main.isEven(int) iteration 33 Unwinding recursion Main.isOdd(int) iteration 34 Unwinding recursion Main.isEven(int) iteration 34 Unwinding recursion Main.isOdd(int) iteration 35 Unwinding recursion Main.isEven(int) iteration 35 Unwinding recursion Main.isOdd(int) iteration 36 Unwinding recursion Main.isEven(int) iteration 36 Unwinding recursion Main.isOdd(int) iteration 37 Unwinding recursion Main.isEven(int) iteration 37 Unwinding recursion Main.isOdd(int) iteration 38 Unwinding recursion Main.isEven(int) iteration 38 Unwinding recursion Main.isOdd(int) iteration 39 Unwinding recursion Main.isEven(int) iteration 39 Unwinding recursion Main.isOdd(int) iteration 40 Unwinding recursion Main.isEven(int) iteration 40 Unwinding recursion Main.isOdd(int) iteration 41 Unwinding recursion Main.isEven(int) iteration 41 Unwinding recursion Main.isOdd(int) iteration 42 Unwinding recursion Main.isEven(int) iteration 42 Unwinding recursion Main.isOdd(int) iteration 43 Unwinding recursion Main.isEven(int) iteration 43 Unwinding recursion Main.isOdd(int) iteration 44 Unwinding recursion Main.isEven(int) iteration 44 Unwinding recursion Main.isOdd(int) iteration 45 Unwinding recursion Main.isEven(int) iteration 45 Unwinding recursion Main.isOdd(int) iteration 46 Unwinding recursion Main.isEven(int) iteration 46 Unwinding recursion Main.isOdd(int) iteration 47 Unwinding recursion Main.isEven(int) iteration 47 Unwinding recursion Main.isOdd(int) iteration 48 Unwinding recursion Main.isEven(int) iteration 48 Unwinding recursion Main.isOdd(int) iteration 49 Unwinding recursion Main.isEven(int) iteration 49 Unwinding recursion Main.isOdd(int) iteration 50 Unwinding recursion Main.isEven(int) iteration 50 Unwinding recursion Main.isOdd(int) iteration 51 Unwinding recursion Main.isEven(int) iteration 51 Unwinding recursion Main.isOdd(int) iteration 52 Unwinding recursion Main.isEven(int) iteration 52 Unwinding recursion Main.isOdd(int) iteration 53 Unwinding recursion Main.isEven(int) iteration 53 Unwinding recursion Main.isOdd(int) iteration 54 Unwinding recursion Main.isEven(int) iteration 54 Unwinding recursion Main.isOdd(int) iteration 55 Unwinding recursion Main.isEven(int) iteration 55 Unwinding recursion Main.isOdd(int) iteration 56 Unwinding recursion Main.isEven(int) iteration 56 Unwinding recursion Main.isOdd(int) iteration 57 Unwinding recursion Main.isEven(int) iteration 57 Unwinding recursion Main.isOdd(int) iteration 58 Unwinding recursion Main.isEven(int) iteration 58 Unwinding recursion Main.isOdd(int) iteration 59 Unwinding recursion Main.isEven(int) iteration 59 Unwinding recursion Main.isOdd(int) iteration 60 Unwinding recursion Main.isEven(int) iteration 60 Unwinding recursion Main.isOdd(int) iteration 61 Unwinding recursion Main.isEven(int) iteration 61 Unwinding recursion Main.isOdd(int) iteration 62 Unwinding recursion Main.isEven(int) iteration 62 Unwinding recursion Main.isOdd(int) iteration 63 Unwinding recursion Main.isEven(int) iteration 63 Unwinding recursion Main.isOdd(int) iteration 64 Unwinding recursion Main.isEven(int) iteration 64 Unwinding recursion Main.isOdd(int) iteration 65 Unwinding recursion Main.isEven(int) iteration 65 Unwinding recursion Main.isOdd(int) iteration 66 Unwinding recursion Main.isEven(int) iteration 66 Unwinding recursion Main.isOdd(int) iteration 67 Unwinding recursion Main.isEven(int) iteration 67 Unwinding recursion Main.isOdd(int) iteration 68 Unwinding recursion Main.isEven(int) iteration 68 Unwinding recursion Main.isOdd(int) iteration 69 Unwinding recursion Main.isEven(int) iteration 69 Unwinding recursion Main.isOdd(int) iteration 70 Unwinding recursion Main.isEven(int) iteration 70 Unwinding recursion Main.isOdd(int) iteration 71 Unwinding recursion Main.isEven(int) iteration 71 Unwinding recursion Main.isOdd(int) iteration 72 Unwinding recursion Main.isEven(int) iteration 72 Unwinding recursion Main.isOdd(int) iteration 73 Unwinding recursion Main.isEven(int) iteration 73 Unwinding recursion Main.isOdd(int) iteration 74 Unwinding recursion Main.isEven(int) iteration 74 Unwinding recursion Main.isOdd(int) iteration 75 Unwinding recursion Main.isEven(int) iteration 75 Unwinding recursion Main.isOdd(int) iteration 76 Unwinding recursion Main.isEven(int) iteration 76 Unwinding recursion Main.isOdd(int) iteration 77 Unwinding recursion Main.isEven(int) iteration 77 Unwinding recursion Main.isOdd(int) iteration 78 Unwinding recursion Main.isEven(int) iteration 78 Unwinding recursion Main.isOdd(int) iteration 79 Unwinding recursion Main.isEven(int) iteration 79 Unwinding recursion Main.isOdd(int) iteration 80 Unwinding recursion Main.isEven(int) iteration 80 Unwinding recursion Main.isOdd(int) iteration 81 Unwinding recursion Main.isEven(int) iteration 81 Unwinding recursion Main.isOdd(int) iteration 82 Unwinding recursion Main.isEven(int) iteration 82 Unwinding recursion Main.isOdd(int) iteration 83 Unwinding recursion Main.isEven(int) iteration 83 Unwinding recursion Main.isOdd(int) iteration 84 Unwinding recursion Main.isEven(int) iteration 84 Unwinding recursion Main.isOdd(int) iteration 85 Unwinding recursion Main.isEven(int) iteration 85 Unwinding recursion Main.isOdd(int) iteration 86 Unwinding recursion Main.isEven(int) iteration 86 Unwinding recursion Main.isOdd(int) iteration 87 Unwinding recursion Main.isEven(int) iteration 87 Unwinding recursion Main.isOdd(int) iteration 88 Unwinding recursion Main.isEven(int) iteration 88 Unwinding recursion Main.isOdd(int) iteration 89 Unwinding recursion Main.isEven(int) iteration 89 Unwinding recursion Main.isOdd(int) iteration 90 Unwinding recursion Main.isEven(int) iteration 90 Unwinding recursion Main.isOdd(int) iteration 91 Unwinding recursion Main.isEven(int) iteration 91 Unwinding recursion Main.isOdd(int) iteration 92 Unwinding recursion Main.isEven(int) iteration 92 Unwinding recursion Main.isOdd(int) iteration 93 Unwinding recursion Main.isEven(int) iteration 93 Unwinding recursion Main.isOdd(int) iteration 94 Unwinding recursion Main.isEven(int) iteration 94 Unwinding recursion Main.isOdd(int) iteration 95 Unwinding recursion Main.isEven(int) iteration 95 Unwinding recursion Main.isOdd(int) iteration 96 Unwinding recursion Main.isEven(int) iteration 96 Unwinding recursion Main.isOdd(int) iteration 97 Unwinding recursion Main.isEven(int) iteration 97 Unwinding recursion Main.isOdd(int) iteration 98 Unwinding recursion Main.isEven(int) iteration 98 Unwinding recursion Main.isOdd(int) iteration 99 Unwinding recursion Main.isEven(int) iteration 99 Unwinding recursion Main.isOdd(int) iteration 100 Unwinding recursion Main.isEven(int) iteration 100 Unwinding recursion Main.isOdd(int) iteration 101 Unwinding recursion Main.isEven(int) iteration 101 Not unwinding recursion Main.isOdd(int) iteration 102 aborting path on assume(false) at file Main.java line 43 function java::Main.main:([Ljava/lang/String;)V bytecode-index 29 thread 0 size of program expression: 6440 steps simple slicing removed 31 assignments Generated 2 VCC(s), 1 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 69309 variables, 353954 clauses SAT checker: instance is UNSATISFIABLE BV-Refinement: got UNSAT, and the proof passes => UNSAT Total iterations: 1 Runtime decision procedure: 0.422748s VERIFICATION SUCCESSFUL EC=42 UNKNOWN