Silicon generates invalid SMT code ("unknown constant") for functions with QP footprint

[aterga]

• Z3 version 4.8.6 - 64 bit

• Silicon revision bc8c538fed426fb973642ff6427ee0b3b4cd629a Jenkins build #2419 (02-Apr-2021)

• Related issue: Silicon generates invalid SMT code ("unknown constant") for QPs in functions #321

The following code:

field val: Int

function snap(g: Set [Ref]): Map[Ref, Int]
    requires (forall n: Ref :: n in g ==> acc(n.val, 1/2))
    ensures forall u:Ref, v:Int :: 
            (u in domain(result) && v == result[u]) ==> (u in g && u.val == v)
    ensures forall u: Ref, F: Set[Ref] ::
            F subset g && u in F ==> u in domain(snap(F)) && snap(F)[u] == u.val

results in the following error:

java.util.concurrent.ExecutionException: viper.silicon.reporting.Z3InteractionFailed: Unexpected output of Z3. Expected 'success' but found: (error "line 912 column 101: unknown constant F@9@00")

[marcoeilers]

This error no longer occurs, so I'll close the issue.