Missing Lit marker on cast to bitvector

[cpitclaudel]

Dafny handles the following two constants differently:

-ghost const SIXTYFOUR: bv128 := 64 as bv128
+ghost const SIXTYFOUR: bv128 := 64

Specifically, the first one doesn't get a Lit marker in Boogie:

--- bv_128_cast.bpl
+++ bv_128_nocast.bpl
@@ -2858,7 +2858,7 @@
   $IsAlloc($o, Tclass._module.__default(), $h)
      <==> $o == null || read($h, $o, alloc));
 
-axiom _module.__default.SIXTYFOUR(): bv128 == 64bv128;
+axiom _module.__default.SIXTYFOUR(): bv128 == Lit(64bv128);

This seems to be a special case of #1912
h/t @seanmcl .