SMT error: select requires as many arguments as the size of the domain

[jspam]

When trying to prove heap.ww from commit 66b6a01c82c76ee2bf748838b6bc3b066e629e4f, the prover fails to verify the postconditions of the function heapInsert because Z3 reports an error along the lines of:

Proof attempt for the calculated formula resulted in Validity UNKNOWN

Prover output was:
(error "line 126 column 21: select requires as many arguments as the size of the domain")
sat
(model 
)

[jspam]

Another test program:

function Boolean first(Boolean[] i)
    _ensures _return = i[0]
{
    return i[0]
}

function Boolean[] test(Boolean[] j)
    _ensures first(_return)
{
    Boolean[] result := j
    result[0] := true
    return result
}

Generated formula:

(assert 
(not 
(forall 
(
(j 
(Array Int Bool))) 
(=> true 

(forall 
    ((_first0 Bool)) 

    (=> 
        (= _first0 (select _first0 0))
        _first0)
    )

))))
(check-sat)
(get-model)

(= _first0 (select _first0 0)) should be (= _first0 (select j 0))

[jspam]

Whoops, my fault: in the previous comment, (= _first0 (select _first0 0)) should not be (= _first0 (select j 0)), but (= _first0 (select result 0)), where result is j with j[0] = 0