Invalid SMT Encoding

[ArquintL]

I came across a program that is happily accepted by Gobra but then results in a Z3 crash ("line 1732 column 214: unknown function/constant sm@29@00"). This happens with the current commit on master: dbe7ff4
Claude Code reduces it to the following minimal example:

// Minimal reproducer for Silicon/Z3 crash: "unknown function/constant sm@...@00"
//
// The crash occurs when ALL of the following are present:
//   1. A ghost struct type with 2+ fields (ValueType)
//   2. A predicate containing a forall quantifier over gpointer[ValueType]
//      with an interface method call as a trigger
//   3. A pure function that unfolds that predicate
//
// Workaround: Replace `ghost struct` with an ADT (see commented-out alternative below).
// With an ADT, the same code verifies without issues.

package reproducer

// CRASH: ghost struct with 2+ fields
ghost type ValueType ghost struct {
    field1 int
    field2 int
}

// WORKAROUND (ADT) – uncomment this and comment out the ghost struct above:
// ghost type ValueType adt {
//     Pair {
//         field1 int
//         field2 int
//     }
// }

type Inv interface {
    ghost
    decreases
    pure TwoStepValueInv(ghost oldValue ValueType, ghost currentValue ValueType) bool
}

ghost type Mutex ghost struct {
    currentValue gpointer[ValueType]
    snapshots    dict[int]gpointer[ValueType]
}

// The forall with trigger `{ inv.TwoStepValueInv(*snapshot, *m.currentValue) }` is essential.
// Removing the second trigger makes the crash go away.
pred (m gpointer[Mutex]) P(inv Inv, client int, currentValue ValueType) {
    acc(m, _) && inv != nil && client elem domain(m.snapshots) && acc((m.snapshots)[client], 1/2) && acc(m.currentValue) && *m.currentValue == currentValue &&
    (forall snapshot gpointer[ValueType] :: { snapshot elem range(m.snapshots) }{ inv.TwoStepValueInv(*snapshot, *m.currentValue) } snapshot elem range(m.snapshots) ==> acc(snapshot, 1/2) && inv.TwoStepValueInv(*snapshot, *m.currentValue))
}

// This pure function triggers the crash via unfolding the predicate above.
// Removing this function makes the crash go away.
ghost
decreases
requires acc(m.P(inv, client, currentValue), _)
pure func (m gpointer[Mutex]) Get(inv Inv, client int, currentValue ValueType) ValueType {
    return unfolding acc(m.P(inv, client, currentValue), _) in *(m.snapshots)[client]
}