./jbmc --propertyfile ../git-sv-benchmarks/java/ReachSafety.prp ../git-sv-benchmarks/java/jpf-regression/ExDarko_false-assert.jar
--------------------------------------------------------------------------------
./jbmc-binary --throw-runtime-exceptions --string-max-input-length 100 --classpath core-models.jar --graphml-witness /tmp/JBMC-log.Y89VeF.witness --unwind 11 --stop-on-fail --64 --object-bits 11 --function Main.main ../git-sv-benchmarks/java/jpf-regression/ExDarko_false-assert.jar
Unwind: 11
JBMC version 5.9 (cbmc-5.7-5176-g7c4b5aa) 64-bit x86_64 linux
Parsing ../git-sv-benchmarks/java/jpf-regression/ExDarko_false-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 2222 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 java::java.lang.Integer::clinit_wrapper iteration 1
aborting path on assume(false) at file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 19 thread 0
size of program expression: 1182 steps
simple slicing removed 1 assignments
Generated 5 VCC(s), 2 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
23698 variables, 29377 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime decision procedure: 0.0240993s
Building error trace
Counterexample:
State 3 thread 0
----------------------------------------------------
__CPROVER_rounding_mode=0 (00000000 00000000 00000000 00000000)
State 4 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_System$$clinit_already_run=false (0)
State 5 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
HIT_return_value=0 (00000000 00000000 00000000 00000000)
State 6 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 7 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float_constarray={ (char)'f', (char)'l', (char)'o', (char)'a', (char)'t' } ({ 00000000 01100110, 00000000 01101100, 00000000 01101111, 00000000 01100001, 00000000 01110100 })
State 8 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float_return_value=0 (00000000 00000000 00000000 00000000)
State 9 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=char_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000000 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 11 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
out=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 12 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int_return_value=0 (00000000 00000000 00000000 00000000)
State 13 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=7, .data=boolean_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000111, 00000000 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 14 thread 0
----------------------------------------------------
Main@class_model={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .isAnnotation=false, .isArray=false,
.isInterface=false, .isSynthetic=false,
.isLocalClass=false, .isMemberClass=false,
.isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 17 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 18 thread 0
----------------------------------------------------
name=&Main.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 19 thread 0
----------------------------------------------------
isAnnotation=false (00000000)
State 20 thread 0
----------------------------------------------------
isArray=false (00000000)
State 21 thread 0
----------------------------------------------------
isInterface=false (00000000)
State 22 thread 0
----------------------------------------------------
isSynthetic=false (00000000)
State 23 thread 0
----------------------------------------------------
isLocalClass=false (00000000)
State 24 thread 0
----------------------------------------------------
isMemberClass=false (00000000)
State 25 thread 0
----------------------------------------------------
isEnum=false (00000000)
State 27 file java/lang/Class.java line 463 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 2 thread 0
----------------------------------------------------
Main@class_model.name=&Main.@java.lang.Object.@class_identifier (00000000 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 29 file java/lang/Class.java line 464 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 5 thread 0
----------------------------------------------------
Main@class_model.isAnnotation=false (00000000)
State 31 file java/lang/Class.java line 465 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 8 thread 0
----------------------------------------------------
Main@class_model.isArray=false (00000000)
State 33 file java/lang/Class.java line 466 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 11 thread 0
----------------------------------------------------
Main@class_model.isInterface=false (00000000)
State 35 file java/lang/Class.java line 467 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 14 thread 0
----------------------------------------------------
Main@class_model.isSynthetic=false (00000000)
State 37 file java/lang/Class.java line 468 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 17 thread 0
----------------------------------------------------
Main@class_model.isLocalClass=false (00000000)
State 39 file java/lang/Class.java line 469 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 20 thread 0
----------------------------------------------------
Main@class_model.isMemberClass=false (00000000)
State 41 file java/lang/Class.java line 470 function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V bytecode-index 23 thread 0
----------------------------------------------------
Main@class_model.isEnum=false (00000000)
State 43 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
HIT={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=3, .data=HIT_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000000 11000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 44 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=void_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000000 11100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 45 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
float={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=5, .data=float_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000101, 00000001 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 46 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=5, .data=short_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000101, 00000001 00100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 47 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=false (0)
State 48 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=6, .data=double_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000110, 00000001 01000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 49 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char_constarray={ (char)'c', (char)'h', (char)'a', (char)'r' } ({ 00000000 01100011, 00000000 01101000, 00000000 01100001, 00000000 01110010 })
State 50 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double_return_value=0 (00000000 00000000 00000000 00000000)
State 51 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean_return_value=0 (00000000 00000000 00000000 00000000)
State 52 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
char_return_value=0 (00000000 00000000 00000000 00000000)
State 53 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=byte_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000001 01100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 54 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte_constarray={ (char)'b', (char)'y', (char)'t', (char)'e' } ({ 00000000 01100010, 00000000 01111001, 00000000 01110100, 00000000 01100101 })
State 55 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short_return_value=0 (00000000 00000000 00000000 00000000)
State 56 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
short_constarray={ (char)'s', (char)'h', (char)'o', (char)'r', (char)'t' } ({ 00000000 01110011, 00000000 01101000, 00000000 01101111, 00000000 01110010, 00000000 01110100 })
State 57 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=3, .data=int_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000011, 00000001 10000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 58 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
int_constarray={ (char)'i', (char)'n', (char)'t' } ({ 00000000 01101001, 00000000 01101110, 00000000 01110100 })
State 59 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=4, .data=long_constarray } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000100, 00000001 10100000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 60 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
byte_return_value=0 (00000000 00000000 00000000 00000000)
State 61 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long_return_value=0 (00000000 00000000 00000000 00000000)
State 62 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
long_constarray={ (char)'l', (char)'o', (char)'n', (char)'g' } ({ 00000000 01101100, 00000000 01101111, 00000000 01101110, 00000000 01100111 })
State 63 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
double_constarray={ (char)'d', (char)'o', (char)'u', (char)'b', (char)'l', (char)'e' } ({ 00000000 01100100, 00000000 01101111, 00000000 01110101, 00000000 01100010, 00000000 01101100, 00000000 01100101 })
State 64 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void_return_value=0 (00000000 00000000 00000000 00000000)
State 65 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
void_constarray={ (char)'v', (char)'o', (char)'i', (char)'d' } ({ 00000000 01110110, 00000000 01101111, 00000000 01101001, 00000000 01100100 })
State 66 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
HIT_constarray={ (char)'H', (char)'I', (char)'T' } ({ 00000000 01001000, 00000000 01001001, 00000000 01010100 })
State 67 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
java$$java_lang_Integer$$clinit_already_run=false (0)
State 68 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
boolean_constarray={ (char)'b', (char)'o', (char)'o', (char)'l', (char)'e', (char)'a', (char)'n' } ({ 00000000 01100010, 00000000 01101111, 00000000 01101111, 00000000 01101100, 00000000 01100101, 00000000 01100001, 00000000 01101110 })
State 69 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
TYPE=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 81 thread 0
----------------------------------------------------
dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 83 thread 0
----------------------------------------------------
dynamic_object1={ .@java.lang.Object={ .@class_identifier="java::array[reference]",
.cproverMonitorCount=0 },
.length=0, .data=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 84 thread 0
----------------------------------------------------
dynamic_object1.length=0 (00000000 00000000 00000000 00000000)
State 87 thread 0
----------------------------------------------------
dynamic_object1.data=dynamic_2_array (00000001 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 88 thread 0
----------------------------------------------------
dynamic_2_array={ null, null, null, null, null } ({ 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 92 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
INPUT arg0a: &dynamic_object1.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 95 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V thread 0
----------------------------------------------------
arg0a=&dynamic_object1.@java.lang.Object.@class_identifier (00000001 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 102 thread 0
----------------------------------------------------
java$$Main$$clinit_already_run=true (1)
State 110 file Main.java line 29 function java::Main.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 111 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 116 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 117 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 122 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 1 thread 0
----------------------------------------------------
this=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 126 file java/lang/Class.java line 184 function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader; bytecode-index 2 thread 0
----------------------------------------------------
cl=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 133 file java/lang/Class.java line 411 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 2 thread 0
----------------------------------------------------
loader=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 138 file java/lang/Class.java line 414 function java::java.lang.Class.desiredAssertionStatus:()Z bytecode-index 6 thread 0
----------------------------------------------------
clazz=&Main@class_model.@java.lang.Object.@class_identifier (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 155 file Main.java line 29 function java::Main.<clinit>:()V bytecode-index 6 thread 0
----------------------------------------------------
$assertionsDisabled=false (00000000)
State 160 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 162 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object13={ .@java.lang.Object={ .@class_identifier="java::Main", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 166 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 170 file Main.java line 29 function java::Main.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 172 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object13.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 181 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 6 thread 0
----------------------------------------------------
this=&dynamic_object13.@java.lang.Object.@class_identifier (00000011 01000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 182 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 6 thread 0
----------------------------------------------------
arg1i=0 (00000000 00000000 00000000 00000000)
State 183 file Main.java line 32 function java::Main.main:([Ljava/lang/String;)V bytecode-index 6 thread 0
----------------------------------------------------
arg2i=2 (00000000 00000000 00000000 00000010)
State 193 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object15={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 195 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 7 thread 0
----------------------------------------------------
dynamic_object15={ .@java.lang.Object={ .@class_identifier="java::Main", .cproverMonitorCount=0 } } ({ { ?, 00000000 00000000 00000000 00000000 } })
State 199 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 9 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 203 file Main.java line 29 function java::Main.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 205 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object15.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 214 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 13 thread 0
----------------------------------------------------
this=&dynamic_object15.@java.lang.Object.@class_identifier (00000011 10100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 215 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 13 thread 0
----------------------------------------------------
arg1i=0 (00000000 00000000 00000000 00000000)
State 216 file Main.java line 33 function java::Main.main:([Ljava/lang/String;)V bytecode-index 13 thread 0
----------------------------------------------------
arg2i=2 (00000000 00000000 00000000 00000010)
State 223 thread 0
----------------------------------------------------
java$$java_lang_Integer$$clinit_already_run=true (1)
State 229 file java/lang/Integer.java line 77 function java::java.lang.Integer.<clinit>:()V bytecode-index 1 thread 0
----------------------------------------------------
i=4 (00000000 00000000 00000000 00000100)
State 238 file java/lang/Class.java line 354 function java::java.lang.Class.getPrimitiveClass:(I)Ljava/lang/Class; bytecode-index 27 thread 0
----------------------------------------------------
className=&int.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 240 thread 0
----------------------------------------------------
c=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 241 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object16={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.name=null, .isAnnotation=false, .isArray=false,
.isInterface=false, .isSynthetic=false,
.isLocalClass=false, .isMemberClass=false,
.isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 243 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object16={ .@java.lang.Object={ .@class_identifier="java::java.lang.Class",
.cproverMonitorCount=0 },
.name=null, .isAnnotation=false, .isArray=false,
.isInterface=false, .isSynthetic=false,
.isLocalClass=false, .isMemberClass=false,
.isEnum=false, .enumConstantDirectory=null } ({ { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 })
State 247 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 2 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 251 file java/lang/Class.java line 39 function java::java.lang.Class.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object16.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 253 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object16.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 257 file java/lang/Class.java line 377 function java::java.lang.Class.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object16.enumConstantDirectory=null (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 260 file java/lang/Class.java line 109 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 3 thread 0
----------------------------------------------------
c=&dynamic_object16.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 262 file java/lang/Class.java line 110 function java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class; bytecode-index 6 thread 0
----------------------------------------------------
dynamic_object16.name=&int.@java.lang.Object.@class_identifier (00000011 11000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 277 file java/lang/Integer.java line 77 function java::java.lang.Integer.<clinit>:()V bytecode-index 2 thread 0
----------------------------------------------------
TYPE=&dynamic_object16.@java.lang.Object.@class_identifier (00000011 11100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 282 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object17={ .@java.lang.Number={ .@class_identifier="java::java.lang.String" },
.value=0 } ({ { ? }, 00000000 00000000 00000000 00000000 })
State 284 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 0 thread 0
----------------------------------------------------
dynamic_object17={ .@java.lang.Number={ .@class_identifier="java::java.lang.Integer" },
.value=0 } ({ { ? }, 00000000 00000000 00000000 00000000 })
State 288 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 3 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Number.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 289 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 3 thread 0
----------------------------------------------------
value=0 (00000000 00000000 00000000 00000000)
State 293 file java/lang/Integer.java line 664 function java::java.lang.Integer.<init>:(I)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Number.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 297 file java/lang/Integer.java line 665 function java::java.lang.Integer.<init>:(I)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object17.value=0 (00000000 00000000 00000000 00000000)
State 305 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object18={ .@java.lang.Number={ .@class_identifier="java::java.lang.String" },
.value=0 } ({ { ? }, 00000000 00000000 00000000 00000000 })
State 307 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object18={ .@java.lang.Number={ .@class_identifier="java::java.lang.Integer" },
.value=0 } ({ { ? }, 00000000 00000000 00000000 00000000 })
State 311 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 7 thread 0
----------------------------------------------------
this=&dynamic_object18.@java.lang.Number.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 312 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 7 thread 0
----------------------------------------------------
value=2 (00000000 00000000 00000000 00000010)
State 316 file java/lang/Integer.java line 664 function java::java.lang.Integer.<init>:(I)V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object18.@java.lang.Number.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 320 file java/lang/Integer.java line 665 function java::java.lang.Integer.<init>:(I)V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object18.value=2 (00000000 00000000 00000000 00000010)
State 326 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 8 thread 0
----------------------------------------------------
this=&dynamic_object17.@java.lang.Number.@class_identifier (00000100 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 327 file Main.java line 44 function java::Main.boxed:(II)V bytecode-index 8 thread 0
----------------------------------------------------
obj=&dynamic_object18.@java.lang.Number.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 344 file java/lang/Integer.java line 789 function java::java.lang.Integer.equals:(Ljava/lang/Object;)Z bytecode-index 7 thread 0
----------------------------------------------------
this=&dynamic_object18.@java.lang.Number.@class_identifier (00000100 00100000 00000000 00000000 00000000 00000000 00000000 00000000)
State 368 file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 16 thread 0
----------------------------------------------------
dynamic_object21={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.String",
.cproverMonitorCount=0 },
.detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } })
State 370 file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 16 thread 0
----------------------------------------------------
dynamic_object21={ .@java.lang.Error={ .@java.lang.Throwable={ .@java.lang.Object={ .@class_identifier="java::java.lang.AssertionError",
.cproverMonitorCount=0 },
.detailMessage=null, .cause=null } } } ({ { { { ?, 00000000 00000000 00000000 00000000 }, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000, 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 } } })
State 374 file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 18 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 378 file java/lang/AssertionError.java line 49 function java::java.lang.AssertionError.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 382 file java/lang/Error.java line 58 function java::java.lang.Error.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 386 file java/lang/Throwable.java line 264 function java::java.lang.Throwable.<init>:()V bytecode-index 1 thread 0
----------------------------------------------------
this=&dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 388 file java/lang/Object.java line 40 function java::java.lang.Object.<init>:()V bytecode-index 2 thread 0
----------------------------------------------------
dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.cproverMonitorCount=0 (00000000 00000000 00000000 00000000)
State 392 file java/lang/Throwable.java line 201 function java::java.lang.Throwable.<init>:()V bytecode-index 4 thread 0
----------------------------------------------------
dynamic_object21.@java.lang.Error.@java.lang.Throwable.cause=&dynamic_object21.@java.lang.Error.@java.lang.Throwable.@java.lang.Object.@class_identifier (00000100 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
Violated property:
file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 19
assertion at file Main.java line 48 function java::Main.boxed:(II)V bytecode-index 19
false
VERIFICATION FAILED
EC=10
FALSE