Hello David,
Le 07/06/2016 à 13:41, David Hauzar a écrit :
> Why3 counterexamples are currently used mainly internally by the SPARK
> tool, but we should indeed put at least some basic documentation to Why3
> manual...
>
> To produce a counterexample, terms (e.g., WhyML variables) must be
> expli
Hello,
Le 18/08/2016 à 10:04, David MENTRE a écrit :
> 2. In my test file, counter example are correctly generated. However,
> in my real life example, no counter example is generated. It appears
> that in this latter case Z3 is killed by why3-cpulimit while in the
> former test case Z3 returns a
Hello,
Le 18/08/2016 à 15:59, David MENTRE a écrit :
> But CVC4 tells me that I have
> non-linear arithmetic so generation of counter-example is disabled.
In fact, this answer of CVC4 is very strange. On the same
counter_example_test.mlw file (attached) on which Z3 can generate
counter examples,
Hello David,
On 18.08.2016 10:04, David MENTRE wrote:
1. In function k in attached WhyML file, there are two "returns"
clause. Two counter examples are generated (for line 26) but for the
second one the counter example is on "s.x" variable while I expected it
on "s.y". Indeed, in function k2 wh
Hello David,
On 18.08.2016 16:18, David MENTRE wrote:
Le 18/08/2016 à 15:59, David MENTRE a écrit :
But CVC4 tells me that I have
non-linear arithmetic so generation of counter-example is disabled.
In fact, this answer of CVC4 is very strange. On the same
counter_example_test.mlw file (attach
-- David MENTRE (2016-08-18)
>
> In fact, this answer of CVC4 is very strange. On the same
> counter_example_test.mlw file (attached) on which Z3 can generate
> counter examples, CVC4 always answer "non linear arith"!
>
> Any idea on what is going on?
CVC4 does not issue counterexamples when non
Hello Yannick,
Le 18/08/2016 à 16:46, Yannick Moy a écrit :
> Hence, for generation of counterexamples, Why3 generates files for CVC4
> that force the use of AUFLIRA (the linear arithmetic case) instead of
> AUFNIRA. If a non-linear operator is used, then CVC4 issues an error,
> which is probably
Hello David,
Le 18/08/2016 à 16:21, David Hauzar a écrit :
>> 2. In my test file, counter example are correctly generated. However,
>> in my real life example, no counter example is generated. It appears
>> that in this latter case Z3 is killed by why3-cpulimit while in the
>> former test case Z3
Hello David,
On 18.08.2016 17:17, David MENTRE wrote:
Clearly, the generated SMT2 file does not set logic to AUFLIRA, as shown
in the used .smt2 file for one goal of my example:
"""
(set-logic AUFBVDTNIRA)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
(set-option
On 18.08.2016 17:20, David MENTRE wrote:
Hello David,
Le 18/08/2016 à 16:21, David Hauzar a écrit :
2. In my test file, counter example are correctly generated. However,
in my real life example, no counter example is generated. It appears
that in this latter case Z3 is killed by why3-cpulimit
Hello David,
Le 18/08/2016 à 16:43, David Hauzar a écrit :
> I am able to get counterexamples with CVC4 in your example:
[...]
> I use the following version of CVC4:
>
> $ cvc4 --version
>
> This is CVC4 version 1.5-prerelease
I confirm that using CVC4 version 1.5-prerelease counter examples ar
-- David Hauzar (2016-08-18)
>
> Yes. We asked CVC4 developers for the support of counterexample generation
> when a time-out limit is reached. But it wouldn't be easy to implement and in
> addition it seems not a priority for them. So maybe it would help if you
> would ask also when you will h
Hello David,
Le 18/08/2016 à 17:51, David Hauzar a écrit :
> Indeed, counterexamples are currently not working with CVC4 1.4 out of
> the box. The driver used for cvc4 1.4 (drivers/cvc4_14) does not include
> the transformation prepare_for_counterexmp which is necessary for
> counterexample genera
Hi,
I just tested the idea of having two timeouts in Alt-Ergo (one for proof
search and another for model search).
It's actually very easy to implement. I get something that seems to work
with about ten lines of code.
But for the moment, Alt-Ergo's output for models is not parsable by
Wh
14 matches
Mail list logo
