What4 backends panic on proof goals involving 0-bit words

[brianhuffman]

Goals with variables of type [0] are handled just fine by the SBV backends, but cause the what4 backends to panic:

sawscript> prove z3 {{ \(x:[0]) y z -> x * (y + z) == x*y + x*z }}
[16:51:35.563] Valid
sawscript> prove w4 {{ \(x:[0]) y z -> x * (y + z) == x*y + x*z }}
saw: You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< ---------------------------------------------------
  Revision:  d52a05c690929bd5ec9d9e27ef0f0674feca40d4
  Branch:    master (uncommited files present)
  Location:  Verifier.SAW.Simulator.Prims
  Message:   Verifier.SAW.Simulator.toWord <<integer>>
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-Hd35jLAFLCP5717Wry3NOP:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:265:13 in saw-core-0.1-Hd35jLAFLCP5717Wry3NOP:Verifier.SAW.Simulator.Prims
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:307:14 in saw-core-0.1-Hd35jLAFLCP5717Wry3NOP:Verifier.SAW.Simulator.Prims
%< ---------------------------------------------------

[robdockins]

This, I think, is due to https://github.com/GaloisInc/saw-core/blob/94c8e51c509cb3379fec3a8710c442b8a2b6ae58/saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs#L57

The case of 0-width bitvectors is translated to the What4 base type Integer, which is bogus. This later lead the variable x to be instantiated at type integer, and this panic results from the type mismatch.

[brianhuffman]

This was fixed in GaloisInc/saw-core#196, which was included in the bump-submodules PR #1212.