On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>
> >> As far as I know, the strategies have not changed since they were
> >> renamed, so I have no idea why you are experiencing a change of behavior
> >> in "Auto level 3".
> >
> > Where are the str
Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>> As far as I know, the strategies have not changed since they were
>> renamed, so I have no idea why you are experiencing a change of behavior
>> in "Auto level 3".
>
> Where are the strategies defined? I found strategies.conf, but that seems
> to h
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 21:31, Julia Lawall a écrit :
> >> * default proof strategies "Auto level 1" and "Auto level 2"
> >> have been respectively renamed "Auto level 2" and "Auto level 3";
> >> "Auto level 1" now behaves similarly to "Auto le
Le 18/03/2020 à 21:31, Julia Lawall a écrit :
>> * default proof strategies "Auto level 1" and "Auto level 2"
>> have been respectively renamed "Auto level 2" and "Auto level 3";
>> "Auto level 1" now behaves similarly to "Auto level 0" but with a longer
>> time limit; more details in
> * default proof strategies "Auto level 1" and "Auto level 2"
> have been respectively renamed "Auto level 2" and "Auto level 3";
> "Auto level 1" now behaves similarly to "Auto level 0" but with a longer
> time limit; more details in the manual, Section 10.6 "Proof Strategies"
> :x
There remains the problem that Auto Level 3 goes into an infinite loop,
at least when the goal is a predicate.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
On Wed, 18 Mar 2020, Claude Marche wrote:
>
>
> Le 18/03/2020 à 14:39, Julia Lawall a écrit :
> > The problem seems ot be the --strings-exp option. If I remove that, cvc4
> > seems to work fine.
>
> Thanks for the feedback. We will do our best to fix this problem in Why3
> development (and prob
Le 18/03/2020 à 14:39, Julia Lawall a écrit :
The problem seems ot be the --strings-exp option. If I remove that, cvc4
seems to work fine.
Thanks for the feedback. We will do our best to fix this problem in Why3
development (and probably a soon upcoming 1.3.1 release...)
Hopefully you can
The problem seems ot be the --strings-exp option. If I remove that, cvc4
seems to work fine.
julia
diff --git a/share/provers-detection-data.conf
b/share/provers-detection-data.conf
index a85e609e4..eac39d396 100644
--- a/share/provers-detection-data.conf
+++ b/share/provers-detection-data.conf
On Wed, 18 Mar 2020, Claude Marche wrote:
>
> Hello,
>
> Le 18/03/2020 à 12:31, Julia Lawall a écrit :
> >>> But the unconditional (get-info :reason-unknown) doesn't look ideal.
> >>
> >> Agreed. Unfortunately, to make it conditional, Why3 would have to
> >> interact with the SMT solvers, that i
Hello,
Le 18/03/2020 à 12:31, Julia Lawall a écrit :
But the unconditional (get-info :reason-unknown) doesn't look ideal.
Agreed. Unfortunately, to make it conditional, Why3 would have to
interact with the SMT solvers, that is, write on stdin, read on stdout,
write on stdin, read on stdout, a
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 12:28, Julia Lawall a écrit :
>
> > What should I do to get why3 to use the right file? I tried rerunning
> > make, but it didn't do anything. Do I need to change my configuration
> > file somehow?
>
> The file that is located t
Le 18/03/2020 à 12:31, Julia Lawall a écrit :
> OK, but then could it be removed? It wasn't there in some previous
> version (concretely, Why3 platform, version 1.2.0+git)
>
> On the other hand, I don't know if it is really there when I am running
> within the IDE.
It should be. The IDE does no
Le 18/03/2020 à 12:28, Julia Lawall a écrit :
> What should I do to get why3 to use the right file? I tried rerunning
> make, but it didn't do anything. Do I need to change my configuration
> file somehow?
The file that is located the "drivers" directory contained in a
directory that is either
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 10:48, Julia Lawall a écrit :
> > When I run cvc4 on the command line, it ends with
> >
> > (error "Can't get-info :reason-unknown when the last result wasn't
> > unknown!")
> >
> > If I remove (get-info :reason-unknown) it ends w
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 09:21, Julia Lawall a écrit :
>
> > 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 w
Le 18/03/2020 à 10:48, Julia Lawall a écrit :
> When I run cvc4 on the command line, it ends with
>
> (error "Can't get-info :reason-unknown when the last result wasn't
> unknown!")
>
> If I remove (get-info :reason-unknown) it ends with unsat (which is not
> what I hoped for, but perhaps I am so
Le 18/03/2020 à 09:21, Julia Lawall a écrit :
> 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?
No, cvc4-realize.drv is never use
When I run cvc4 on the command line, it ends with
(error "Can't get-info :reason-unknown when the last result wasn't
unknown!")
If I remove (get-info :reason-unknown) it ends with unsat (which is not
what I hoped for, but perhaps I am somehow not running it properly).
But the unconditional (get-
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, her
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, her
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-detecti
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.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
23 matches
Mail list logo
