Closed jensgerlach closed 3 years ago
@jensgerlach I could potentially add such an option but before doing so, I would like to understand what issues you are experiencing with CVC4 1.7. If possible, I would rather fix issues with CVC4 1.7 than adding an option to use 1.6 because 1.7 includes critical bug fixes. It would also be great if everyone could profit from having the fixes in 1.7. I hope this makes sense.
I suspect that it is related to a feature called sessions in Frama-C/WP
but I will look more carefully.
If I don't use sessions then cvc4 (1.7) seems to work fairly well although it is not officially supported by version 1.2.1 of Why3 to which Frama-C
is currently tied.
I have check the issue. The problem I experienced appears not to be related with cvc4 1.7
.
I also could fix the problems I experienced.
Nevertheless, I would appreciate if there would be a simple way to install cvc4 1.6
.
(For example, providing a macOS binary on the download page.)
As I explained above, it is often not feasible to use the newest release of an automatic prover with Frama-C or Why3.
Thanks in advance!
I have finally uploaded 1.6 binaries for macOS here: https://github.com/CVC4/CVC4/releases/tag/1.6 . All the dependencies are linked statically except the system libraries. Please let me know if that binary works for you.
Thanks a lot for the binary. We have, however, in the meantime migrated to CVC4 1.7 both on macOS and linux. Still, I think it is a good idea to not only provide the latest version but also at least the previous version of CVC4.
Since you've moved to a newer version and we now offer binary downloads of older versions, I am closing this issue. Thanks again for the report.
Hello,
thanks for providing the update to version 1.7. However, I am experiencing several issues with using CVC4 1.7 together with Frama-C 20.0 (in particular while preparing a new release of ACSL by Example).
Is there a simple way, to downgrade CVC4 to version 1.6 using homebrew?
Thanks in advance!
Jens