SBV error from unint_z3 when showing counterexamples

[brianhuffman]

When you run the following saw-script:

let {{
  foo : [8] -> [8]
  foo x = x
}};

prove_print (unint_z3 ["foo"]) {{ \x -> foo x == x }};

you get the following error message from SBV:

*** Data.SBV: Unexpected response from the solver, context: get-value:
***
***    Sent      : (get-value (|foo#48|))
***    Expected  : a function value
***    Received  : (error "line 17 column 12: invalid function application, missing arguments foo#48")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 17 column 12: invalid function application, missing arguments foo#48"

I'm not sure whether this is a bug in SAW, or in the SBV library.

[atomb]

I think this is missing functionality in SBV. From what I understand, there's not a solid standard for how solvers should return models of uninterpreted functions, so every solver does it differently and in an undocumented (although generally straightforward) way.

Interestingly, using w4_unint_z3 instead yields a straightforward counterexample x = 0, but it just leaves out the model for foo.

[brianhuffman]

So can we work around this from our end? Can we avoid asking SBV about models for uninterpreted function symbols?

[weaversa]

The error message from SBV is now slightly different.

sawscript> let {{ foo x = x : [8] }}
sawscript> prove_print (unint_z3 ["foo"]) {{ \x -> foo x == x }};
saw: 
*** Data.SBV: Unexpected response from the solver, context: get-value:
***
***    Sent      : (get-value (|foo#50|))
***    Expected  : a function value
***    Received  : ((|foo#50| ((as const Array) #x00)))
***
***    Executable: z3
***    Options   : -nw -in -smt2

[brianhuffman]

See also GaloisInc/what4#39