479 do not backtranslate fancy sorts in get-model

[jberthold]

Values of any sort other than SortBool and SortInt cannot currently be back-translated from the SMT representation (all sorts unknown to the solver are opaque). In particular, this is true for Map-sorted values (which are used frequently in EVM).

• Do not attempt to back-translate values of sorts other than SortBool and SortInt
• but still include the related SMT variables in the get-values requestl;
• and indicate untranslated variables by adding VAR = VAR to the returned substitution.

As shown in the added integration test, there are cases where the Map-sorted value is relevant, but cannot currently be returned. We might consider modeling Maps specifically as arrays in the SMT solver in the future.

Fixes runtimeverification/kontrol#479

[jberthold]

Unsure about this but I thought it might be helpful to indicate in the response that some potentially-relevant variables are not included.

[palinatolmach]

Thanks @jberthold, will try it out in a bit!

[palinatolmach]

The result looks great to me! I just ran Kontrol with this version of Booster on the test used in runtimeverification/kontrol#479, and here's the counterexample I'm getting

  Path condition:
    { true #Equals VV0_from_114b9705:Int ==Int 0 }
  Model:
    VV2_amount_114b9705 = 0
    TIMESTAMP_CELL = 0
    ORIGIN_ID = 10
    CALLER_ID = 10
    CONTRACT_ID = 2
    VV0_from_114b9705 = 0
    NUMBER_CELL = 0
    VV1_to_114b9705 = 1
    ?STORAGE = ?STORAGE:Map

which I think looks great, and it should be clear to the user that we don't concretize ?STORAGE values.

I'll leave it to @goodlyrottenapple and @geo2a to approve :)