Invalid smt: `unknown function/constant sm@24@00`

[pieter-bos]

Possible duplicate of #541 or #321, but seems closer to (closed) #295

This file:

domain array {
  function loc(a: array, i: Int): Ref
  function len(a: array): Int
  function loc_inv_1(loc: Ref): array
  function loc_inv_2(loc: Ref): Int
  
  axiom {
    (forall a: array, i: Int :: { loc(a, i) } loc_inv_1(loc(a, i)) == a && loc_inv_2(loc(a, i)) == i)
  }
  
  axiom {
    (forall a: array :: { len(a) } len(a) >= 0)
  }
}

field int: Int

function correctness_upto(parent: array, left: array, root: Int): Bool
  requires (forall i: Int :: 0 <= i && i < len(left) ==> acc(loc(left, i).int, 1/2))
  requires (forall i: Int :: 0 <= i && i < len(parent) ==> acc(loc(parent, i).int, 1/2))
  requires correctness_invar(left)
{
  (forall i: Int :: { loc(parent, i).int } 0 <= i && i < len(parent) ==> loc(parent, i).int == 0) && 
  (forall i: Int :: { loc(parent, i).int } 0 <= i && i < len(parent) ==> loc(parent, i).int == 0)
}

function correctness_invar(left: array): Bool
  requires (forall i: Int :: { loc(left, i).int } (0 <= i && i < len(left)) ==> acc(loc(left, i).int, 1/2))
{ true }

Reports:

Silicon found 1 error in 3.66s:
  [0] Interaction with prover (instance 01) failed: Unexpected output of prover. Expected 'success' but found: (error "line 985 column 106: unknown function/constant sm@24@00")

[marcoeilers]

Fixed in PR #654