Inefficient encoding of matches in Boogie

[sonmarcho]

Consider the following Dafny code:

datatype T = | V0 | V1 | V2 | V3 | V4 | V5 | V6 | V7 | V8 | V9

predicate method P(v: T)
{
  match v
    case V0 => true
    case _ => false
}

In Boogie, the P predicate gets compiled to the following nested if then else:

// definition axiom for _module.__default.P for all literals (revealed)
axiom 1 <= $FunctionContextHeight
   ==> (forall v#0: DatatypeType :: 
    {:weight 3} { _module.__default.P(Lit(v#0)) } 
    _module.__default.P#canCall(Lit(v#0))
         || (1 != $FunctionContextHeight && $Is(v#0, Tclass._module.T()))
       ==> _module.__default.P(Lit(v#0))
         == (if _module.T.V0_q(Lit(v#0))
           then true
           else (if _module.T.V1_q(Lit(v#0))
             then false
             else (if _module.T.V2_q(Lit(v#0))
               then false
               else (if _module.T.V3_q(Lit(v#0))
                 then false
                 else (if _module.T.V4_q(Lit(v#0))
                   then false
                   else (if _module.T.V5_q(Lit(v#0))
                     then false
                     else (if _module.T.V6_q(Lit(v#0))
                       then false
                       else (if _module.T.V7_q(Lit(v#0))
                         then false
                         else (if _module.T.V8_q(Lit(v#0)) then false else false))))))))));

We would rather expect the following more efficient encoding:

axiom 1 <= $FunctionContextHeight
   ==> (forall v#0: DatatypeType :: 
    {:weight 3} { _module.__default.P(Lit(v#0)) } 
    _module.__default.P#canCall(Lit(v#0))
         || (1 != $FunctionContextHeight && $Is(v#0, Tclass._module.T()))
       ==> _module.__default.P(Lit(v#0))
         == (if _module.T.V0_q(Lit(v#0))
           then true
           else false));

I detected this issue when working on a bug which led to the minimal example below: in the following instance, the encoding of P1 contains 10 * 10 = 100 cases, which actually leads to a stack overflow in Boogie.

predicate method P1(v: T, v': T)
{
  match (v, v')
    case (V0, V0) => true
    case (V1, V1) => true
    case (V2, V2) => true
    case (V3, V3) => true
    case (V4, V4) => true
    case (V5, V5) => true
    case (V6, V6) => true
    case (V7, V7) => true
    case (V8, V8) => true
    case (V9, V9) => true
    case _ => false
}

lemma L(v: T)
  requires P1(v, v)
  requires P1(v, v)
  requires P1(v, v)
  requires P1(v, v)
{}

// This triggers a stack overflow
lemma L1(v: T)
{
  L(v);
}