search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

CVC5 no longer supports --model-witness-value command line option #626

Closed LeventErkok closed 2 years ago

LeventErkok commented 2 years ago

Looks like CVC5 dropped the command-line option --model-witness-value which makes it unusable from SBV.

Workaround: Use the environment variable SBV_CVC5_OPTIONS, thusly:

$ SBV_CVC5_OPTIONS="--lang smt --incremental --no-interactive" ghci
Prelude> :m + Data.SBV
Prelude Data.SBV> proveWith cvc5 $ \x -> x.== x + (1::SWord8)
Falsifiable. Counter-example:
  s0 = 0 :: Word8

The real-fix will be figuring out if they renamed it to something else and using that option, or if they completely removed it figure out what the impact on SBV is. (I vaguely recall this had something to do with models with SReal values, but can't recall it exactly now.)

d-xo commented 2 years ago

Thanks! This worked for me.

LeventErkok commented 2 years ago

Asked at https://github.com/cvc5/cvc5/issues/8898, will make the corresponding modifications to SBV based on their response.

LeventErkok commented 2 years ago

@d-xo Looks like CVC5 will no longer support this option; so I removed it from SBV.

d-xo commented 2 years ago

Thanks for the fix!

LeventErkok commented 2 years ago

@d-xo Looks like CVC5 has new support for algebraic-reals, see https://github.com/cvc5/cvc5/issues/8898#issuecomment-1187472197. (They added a new option --nl-cov with new model output.)

Not sure if that's something you cared about. I'll be adding support for this in SBV in the coming weeks.