Crash when last two implicit arguments have dependency

[mtzguido]

assume val p : x:int -> v1:int -> v2:int -> vprop

assume val f : x:int -> #v1:int -> #v2:int{v2 > v1} -> 
                stt unit (p x v1 v2) (fun _ -> emp)

fn test (_:unit)
  requires p 1 2 4
  ensures emp
  {
    f 1
  }

Gives:

  - "uncaught exception: Failure("Failed to find v1@1\nEnv is (., dummy)\n")"