pact icon indicating copy to clipboard operation
pact copied to clipboard

FV fails with SBV == 8.4

Open emilypi opened this issue 6 years ago • 1 comments

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!

emilypi avatar Oct 02 '19 22:10 emilypi

SBV is now at 9.0.

jwiegley avatar Dec 21 '22 16:12 jwiegley