--- a/src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java	Wed Apr 22 15:54:26 2015 -0700
@@ -41,9 +41,12 @@
     arrayRef = frame.peek(1); // ..,arrayRef,idx
     if (arrayRef == MJIEnv.NULL) {
       return ti.createAndThrowException("java.lang.NullPointerException");
-    }    
+    }
     ElementInfo eiArray = ti.getElementInfo(arrayRef);
-    
+
+    indexOperandAttr = peekIndexAttr(ti);
+    arrayOperandAttr = peekArrayAttr(ti);
+
     Scheduler scheduler = ti.getScheduler();
     if (scheduler.canHaveSharedArrayCG( ti, this, eiArray, index)){ // don't modify the frame before this
       eiArray = scheduler.updateArraySharedness(ti, eiArray, index);
@@ -85,6 +88,11 @@
     return ti.getTopFrame().peek(1);
   }
 
+  @Override
+  public Object peekArrayAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr(1);
+  }
+
   // wouldn't really be required for loads, but this is a general
   // ArrayInstruction API
   @Override
@@ -92,6 +100,11 @@
     return ti.getTopFrame().peek();
   }
 
+  @Override
+  public Object peekIndexAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr();
+  }
+
   protected abstract void push (StackFrame frame, ElementInfo e, int index)
                 throws ArrayIndexOutOfBoundsExecutiveException;
 

--- a/src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java	Wed Apr 22 15:54:26 2015 -0700
@@ -34,13 +34,17 @@
  */
 public abstract class ArrayStoreInstruction extends JVMArrayElementInstruction implements StoreInstruction, JVMInstruction {
 
+
   @Override
   public Instruction execute (ThreadInfo ti) {
     StackFrame frame = ti.getModifiableTopFrame();
     int idx = peekIndex(ti);
     int aref = peekArrayRef(ti); // need to be polymorphic, could be LongArrayStore
     ElementInfo eiArray = ti.getElementInfo(aref);
-        
+
+    arrayOperandAttr = peekArrayAttr(ti);
+    indexOperandAttr = peekIndexAttr(ti);
+
     if (!ti.isFirstStepInsn()){ // first execution, top half
       //--- runtime exceptions
       if (aref == MJIEnv.NULL) {
@@ -93,6 +97,18 @@
     return ti.getTopFrame().peek(1);
   }
 
+  // override in LongArrayStoreInstruction
+  @Override
+  public Object  peekArrayAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr(2);
+  }
+
+  @Override
+  public Object peekIndexAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr(1);
+  }
+
+
   protected abstract void popValue(StackFrame frame);
  
   protected abstract void setField (ElementInfo e, int index)

--- a/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/JVMArrayElementInstruction.java	Wed Apr 22 15:54:26 2015 -0700
@@ -29,13 +29,20 @@
   
   protected int arrayRef;
   protected int index; // the accessed element
+
+  // we cache these to avoid the need for executeInstruction() listening
+  // if attrs are processed in instructionExecuted()
+  protected Object arrayOperandAttr;
+  protected Object indexOperandAttr;
   
   // we need this to be abstract because of the LongArrayStore insns
   @Override
   abstract public int peekIndex (ThreadInfo ti);
-  
-  abstract protected int peekArrayRef (ThreadInfo ti);
-  
+  abstract public int peekArrayRef (ThreadInfo ti);
+
+  abstract public Object peekIndexAttr (ThreadInfo ti);
+  abstract public Object peekArrayAttr (ThreadInfo ti);
+
   public boolean isReferenceArray() {
     return false;
   }
@@ -62,6 +69,23 @@
     }
   }
 
+  public Object getArrayOperandAttr (ThreadInfo ti){
+    if (ti.isPreExec()) {
+      return peekArrayAttr(ti);
+    } else {
+      return arrayOperandAttr;
+    }
+  }
+
+  public Object getIndexOperandAttr (ThreadInfo ti){
+    if (ti.isPreExec()) {
+      return peekIndexAttr(ti);
+    } else {
+      return indexOperandAttr;
+    }
+  }
+
+
   @Override
   public ElementInfo peekArrayElementInfo (ThreadInfo ti){
     int aref = getArrayRef(ti);

--- a/src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java	Wed Apr 22 15:54:26 2015 -0700
@@ -54,7 +54,18 @@
   public int peekIndex(ThreadInfo ti){
     return ti.getTopFrame().peek(2);
   }
-  
+
+  @Override
+  public Object  peekArrayAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr(3);
+  }
+
+  @Override
+  public Object peekIndexAttr (ThreadInfo ti){
+    return ti.getTopFrame().getOperandAttr(2);
+  }
+
+
   @Override
   public void accept(JVMInstructionVisitor insVisitor) {
 	  insVisitor.visit(this);

--- a/src/main/gov/nasa/jpf/listener/VarTracker.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/listener/VarTracker.java	Wed Apr 22 15:54:26 2015 -0700
@@ -25,6 +25,7 @@
 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
 import gov.nasa.jpf.jvm.bytecode.GETFIELD;
 import gov.nasa.jpf.jvm.bytecode.GETSTATIC;
+import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
 import gov.nasa.jpf.report.ConsolePublisher;
@@ -39,6 +40,7 @@
 import gov.nasa.jpf.vm.MethodInfo;
 import gov.nasa.jpf.vm.StackFrame;
 import gov.nasa.jpf.vm.ThreadInfo;
+import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 
 import java.io.PrintWriter;
 import java.util.ArrayList;
@@ -159,17 +161,14 @@
 
     queue.clear();
   }
-  
-  
+
   // <2do> - general purpose listeners should not use types such as String for storing
   // attributes, there is no good way to make sure you retrieve your own attributes
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     String varId;
-    
-    if ( ((((executedInsn instanceof GETFIELD) || (executedInsn instanceof GETSTATIC)))
-            && ((JVMFieldInstruction)executedInsn).isReferenceField()) ||
-         (executedInsn instanceof ALOAD)) {
+
+    if (executedInsn instanceof ALOAD) {
       // a little extra work - we need to keep track of variable names, because
       // we cannot easily retrieve them in a subsequent xASTORE, which follows
       // a pattern like:  ..GETFIELD.. some-stack-operations .. xASTORE
@@ -178,27 +177,34 @@
       if (objRef != MJIEnv.NULL) {
         ElementInfo ei = ti.getElementInfo(objRef);
         if (ei.isArray()) {
-          varId = ((LocalVariableInstruction)executedInsn).getVariableId();
-          
+          varId = ((LocalVariableInstruction) executedInsn).getVariableId();
+
           // <2do> unfortunately, we can't filter here because we don't know yet
           // how the array ref will be used (we would only need the attr for
           // subsequent xASTOREs)
           frame = ti.getModifiableTopFrame();
-          frame.addOperandAttr( varId);
+          frame.addOperandAttr(varId);
         }
       }
-    }
+
+    } else if ((executedInsn instanceof ReadInstruction) && ((JVMFieldInstruction)executedInsn).isReferenceField()){
+      varId = ((JVMFieldInstruction)executedInsn).getFieldName();
+
+      StackFrame frame = ti.getModifiableTopFrame();
+      frame.addOperandAttr(varId);
+
+
     // here come the changes - note that we can't update the stats right away,
     // because we don't know yet if the state this leads into has already been
     // visited, and we want to detect only var changes that lead to *new* states
-    // (objective is to find out why we have new states)
-    else if (executedInsn instanceof StoreInstruction) {
+    // (objective is to find out why we have new states). Note that variable
+    // changes do not necessarily contribute to the state hash (@FilterField)
+  } else if (executedInsn instanceof StoreInstruction) {
       if (executedInsn instanceof ArrayStoreInstruction) {
         // did we have a name for the array?
         // stack is ".. ref idx [l]value => .."
         // <2do> String is not a good attribute type to retrieve
-        StackFrame frame = ti.getTopFrame();
-        String attr = frame.getOperandAttr(1, String.class);
+        Object attr = ((ArrayStoreInstruction)executedInsn).getArrayOperandAttr(ti);
         if (attr != null) {
           varId = attr + "[]";
         } else {
@@ -207,11 +213,18 @@
       } else {
         varId = ((LocalVariableInstruction)executedInsn).getVariableId();
       }
-      
-      if (isMethodRelevant(executedInsn.getMethodInfo()) && isVarRelevant(varId)) {
-        queue.add(new VarChange(varId));
-        lastThread = ti;
-      }
+      queueIfRelevant(ti, executedInsn, varId);
+
+    } else if (executedInsn instanceof WriteInstruction){
+      varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+      queueIfRelevant(ti, executedInsn, varId);
+    }
+  }
+
+  void queueIfRelevant(ThreadInfo ti, Instruction insn, String varId){
+    if (isMethodRelevant(insn.getMethodInfo()) && isVarRelevant(varId)) {
+      queue.add(new VarChange(varId));
+      lastThread = ti;
     }
   }
 

--- a/src/main/gov/nasa/jpf/vm/NativePeer.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/NativePeer.java	Wed Apr 22 15:54:26 2015 -0700
@@ -407,7 +407,7 @@
     return annotation.noOrphanWarning();
   }
   
-  private static MethodInfo searchMethod (String mname, MethodInfo[] methods) {
+  private MethodInfo searchMethod (String mname, MethodInfo[] methods) {
     int idx = -1;
 
     for (int j = 0; j < methods.length; j++) {
@@ -419,7 +419,7 @@
         if (idx == -1) {
           idx = j;
         } else {
-          throw new JPFException("overloaded native method without signature: " + mname);
+          throw new JPFException("overloaded native method without signature: " + ci.getName() + '.' + mname);
         }
       }
     }

--- a/src/main/gov/nasa/jpf/vm/StackFrame.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/StackFrame.java	Wed Apr 22 15:54:26 2015 -0700
@@ -499,7 +499,7 @@
     assert (top >= stackBase);
     
     if ((attrs != null)){
-      return ObjectList.getFirst( attrs[top], attrType);
+      return ObjectList.getFirst(attrs[top], attrType);
     }
     return null;
   }
@@ -604,9 +604,9 @@
    */
   public <T> T getOperandAttr (int offset, Class<T> attrType){
     int i = top-offset;
-    assert (i >= stackBase);
+    assert (i >= stackBase) : this;
     if (attrs != null){
-      return ObjectList.getFirst( attrs[i], attrType);
+      return ObjectList.getFirst(attrs[i], attrType);
     }
     return null;
   }

--- a/src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java	Tue Apr 21 00:34:15 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/bytecode/ReadInstruction.java	Wed Apr 22 15:54:26 2015 -0700
@@ -19,9 +19,9 @@
 package gov.nasa.jpf.vm.bytecode;
 
 /**
- * common type for all xGET insns
+ * common type for all GETx insns
  * This has to be an interface since implementors have to be derived from the abstract FieldInstruction
  */
-public interface ReadInstruction extends ReadOrWriteInstruction, StoreInstruction {
+public interface ReadInstruction extends ReadOrWriteInstruction {
   // nothing here yet
 }