Multiple jvm_field_is declarations on same field are not detected

[brianhuffman]

Using this java source file:

class Test
{
    long val;
    long get () {
        return val;
    }
    void set (long x) {
        val = x;
    }
}

and this .saw file:

crucible_jvm_verify test "get" [] false
  do {
    this <- jvm_alloc_object "Test";
    val <- jvm_fresh_var "val" java_long;
    jvm_field_is this "val" (jvm_term val);
    jvm_field_is this "val" (jvm_term {{ 0 : [64] }});
    jvm_execute_func [this];
    jvm_return (jvm_term val);
  } z3;

the proof succeeds, even though it should fail with an error about multiple points-to constraints on the same field.