On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 08:45, Julia Lawall a écrit :
> > Could the generated code be bigger than before? I tried cvc4 on a proof
> > that is simple and has few dependencies and it was fine.
>
> Among the things that changed recently regarding CVC4, here are a few
> things you could try:
>
> - In share/prover-detection-data.conf, in the block for CVC4 1.7 (plain
> "cvc4", not "cvc4-ce"), remove the "--strings-exp" command-line option.
>
> - Similarly, remove the "--stats" option.
>
> - In drivers/cvc4_17.drv, replace "ALL_SUPPORTED" by "AUFBVFPDTSNIRA".
I have the impression that it is using drivers/cvc4-realize.drv. I made
the change you suggested, but if I edit the cvc4 proof, it shows
ALL_SUPPORTED. Or is drivers/cvc4-realize.drv what is used when editing?
julia
>
> Best regards,
>
> Guillaume
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
