#32 Thread is not interrupted

[Vadim]

JPF does not interrupt thread, because it thinks that
it is not in waiting state.

I'm creating a thread in the main method which calls
wait in it's run method. Then I'm interrupting the
created thread. When I'm running this example under
regular JVM (SUN JRE 1.4) the thread interrupts with
InterruptedException (and throws uncaught
RuntimeException). But when I'm running the same code
under JVM^JPF, JPF does not find this execution path
(on which the exception is thrown).

For the code bellow under SUN JRE I have:
------------------------------------------
thread interrupted
finished
java.lang.RuntimeException: bug
at InterruptedThread$1.run
(InterruptedThread.java:17)
------------------------------------------

and for the JPF:
------------------------------------------
finished
finished
===================================
No Errors Found
===================================
------------------------------------------

The code:
------------------------------------------
public class InterruptedThread {

static Object obj = new Object();

static int icount = 0;

public static void main(String[] args) {
Thread t1 = new Thread() {
public void run() {
synchronized(obj) {
icount++;
try {

obj.wait();

} catch
(InterruptedException e) {

System.out.println("thread interrupted");
throw
new RuntimeException("bug");
}
}
}
};

t1.start();
t1.interrupt();

while(true)
synchronized (obj) {
if(icount==1) {
obj.notifyAll
();
break;
}
}

try {
t1.join();
} catch (InterruptedException e) {
System.out.println("join
interrupted");
}
System.out.println("finished");
}
}
------------------------------------------

[Vadim]

Java source class