milos, jpf still havent developed low mechanism abstractions ,some methods that use the native librarires will be ignored by jpf the field.set function uses the same native library abstraction .thus every block of code that uses these will give JPF Exception as in this case Illegal Argument Exception . please go through this https://babelfish.arc.nasa.gov/trac/jpf/wiki/devel/mji#no1 I hope this helped you.
please have a look .
the problem here is in the cast function in the src/classes/java.lang/class.java file in jpf source code. actually, it was using the following implementation, public T cast(Object obj){ if(o!=null && !instanceof(o)){ throws new ClassCastException(); } return (T)o; } here ,the instanceof() function is a native function and its implementation certainly is not working properly. so ,what i did was I modified the function as public T cast(Object o){ try{ return (T)o; } catch(ClassCastException e){ throw...