pact
pact copied to clipboard
FV fails with SBV == 8.4
The following errors are returned, and verification fails where before it succeeded:
coin.pact:322:23:Warning:
*** Data.SBV: Unexpected non-success response from Z3:
***
*** Sent : (set-option :model.inline_def true )
*** Expected : success
*** Received : (error "line 9 column 31: unknown parameter 'inline_def' at module 'model'
*** Legal parameters are:
*** compact (bool) (default: false)
*** completion (bool) (default: false)
*** partial (bool) (default: false)
*** v1 (bool) (default: false)
*** v2 (bool) (default: false)")
***
*** Exit code : ExitFailure (-15)
*** Executable: /usr/local/bin/z3
*** Options : -nw -in -smt2
***
*** Reason : Backend solver reports it does not support this option.
*** Check the spelling, and if correct please report this as a
*** bug/feature request with the solver!
SBV is now at 9.0.