FV Failure with (select) Function in Pact Modules

[chicodias]

When using the (select) function within a module, the formal verification (FV) fails, even though the schema appears to be correct. The error message indicates an OutputFailure: Analysis doesn't support this construct yet, which is confusing, because the error seems unrelated to the schema itself. This issue seems similar to #1114, however I'm using last versions of pact and z3.

It would be nice to have the (select) function to be properly supported by the FV or to have a clearer error message that accurately describes the issue. Ideally, the FV should handle (select) without failing, as it is a common and essential database operation in smart contracts.

As an alternative, improving the error messaging and the documentation to indicate that (select) is not currently supported by the FV would help developers understand the limitation without confusion.

Additional context

Using Z3 version 4.13.1 - 64 bit and Pact version 4.11.

Here’s the example code that works:

(module B G
  (defcap G() true)
  (defschema s
      @doc "test"
      a:string
      b:decimal
      c:integer
  )
  (deftable t:{s})
)

pact> (verify "B")
"Verification of B succeeded"

And here’s the code that fails upon adding the (select) function:

(module B G
  (defcap G() true)
  (defschema s
      @doc "test"
      a:string
      b:decimal
      c:integer
  )
  (deftable t:{s})
  (defun f()
    (select t (constantly true))
  )
)

pact> (verify "B")
"Verification of B failed"
OutputFailure: Analysis doesn't support this construct yet: Table B.t1::table:{B.s}