opaque leaked through consequence axiom

[Chris-Hawblitzel]

The following code defines an opaque predicate p and never reveals p, but it still manages to prove something that should only be provable if p is revealed:

predicate {:opaque} p(i:int)
{
  i == 3
}

predicate {:opaque} q(x:int)
  requires p(x)
  ensures  p(x)
{
  true
}

lemma L(x:int)
  requires p(x)
{
  reveal_q();
  assert q(x);
  assert x == 3; // succeeds; should fail
}

I think the consequence axiom for q unintentionally reveals p by using q's fuel ($ly) instead of the start fuel for p:

// consequence axiom for _module.__default.q
axiom 0 < $ModuleContextHeight
     || (0 == $ModuleContextHeight && 1 <= $FunctionContextHeight)
   ==> (forall $ly: LayerType, $Heap: Heap, x#0: int :: 
    { _module.__default.q($ly, $Heap, x#0) } 
    _module.__default.q#canCall($Heap, x#0)
         || ((0 != $ModuleContextHeight || 1 != $FunctionContextHeight)
           && $IsGoodHeap($Heap)
           && _module.__default.p($ly, $Heap, x#0))
       ==> _module.__default.p($ly, $Heap, x#0));