team-worthwhile/worthwhile — Issue #108: SMT error: select requires as many arguments as the size of the domain
Author: jspam
Created: 2012-03-02 21:34:46+00:00
State: open
Labels: prover

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
)
```