Unexpected non-success response from Yices

[msaaltink]

With the bv module from cryptol-specs:

$ cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.9.1 (c29a9ce)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :m Common::bv
Loading module Cryptol
Loading module Common::bv
Common::bv> :set prover=yices
Common::bv> :prove \(x:[8]) y -> toInteger (safe_product (x,y)) == (toInteger x) * (toInteger y)

SBV exception:

*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (define-fun s6 () Int (bv2nat s5))
***    Expected  : success
***    Received  : (error "at line 10, column 24: undefined term: bv2nat")
***
***    Exit code : ExitSuccess
***    Executable: /home/mark/bin/yices-smt2
***    Options   : --incremental
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

This does not occur if the solver is z3.

[brianhuffman]

As I recall, Cryptol is using an SBV-provided function to implement toInteger in the proof backend. And I believe that SBV function uses the SMTLib bv2nat function in those solvers that support it. I would guess that this error is happening because of a mismatch between your Yices version and the version that SBV is expecting (which in turn depends on the version of SBV that your Cryptol binary was compiled with).

[brianhuffman]

Well, I just checked a few version combinations of SBV and yices, and this error pops up with every combination I tried: SBV 8.6 and 8.7 (the only versions allowed by cryptol.cabal), and yices 2.6.1 and 2.6.2 (which I believe is the latest release).

@LeventErkok, does SBV expect yices to support bv2nat, or is this a sign that we're somehow using the library incorrectly?

[LeventErkok]

@brianhuffman

bv2nat is part of the official SMTLib logic for bitvectors: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

Looks like Yices doesn't support it though. (SBV is really only tested with z3, there are only a few tests for other solvers. So, it's not surprising this didn't come up before.)

I suggest you file this as an issue with the Yices folks (https://github.com/SRI-CSL/yices2/issues) and see what they have to say about it. If they have an alternate translation, there are mechanisms in SBV to put in that. If they don't support it at all, we can still support it by doing the conversion ourselves directly within SBV, but it'd be best if they supported this out-of-the-box for obvious reasons.

[atomb]

I'll note that there is a Yices issue for this now: https://github.com/SRI-CSL/yices2/issues/359