[Why3-club] Count-example generation attempts with Z3 and CVC4

David MENTRE dmentre at linux-france.org
Thu Aug 18 15:59:16 CEST 2016


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 an output by itself before the time limit.
[...]
> Do you know a way to generate a counter-example when time limit is
> reached? By playing with Z3 options (e.g. using option -T)? Would it be
> the same with CVC4? How do you handle the case in SPARK?

I played a bit with Z3 and CV4, bypassing why3-cpulimit. Z3 is still
silent when asked for a counter example. But CVC4 tells me that I have
non-linear arithmetic so generation of counter-example is disabled.

CVC4 output:
"""
Call_provers: command is: cvc4 --tlimit-per=1000 --lang=smt2

/tmp/why_e71095_carriagemnlinemncontrolmnce-T-WP_parameter_carriage_line_control_cycle.smt2
Call_provers: exited with status 0
Call_provers: prover output:
SmtEngine: turning off produce-models because unsupported for nonlinear
arith
unknown
(:reason-unknown incomplete)

Call_provers: model:
Call_provers:
carriage-line-control-ce.mlw Carriage_Line_Control WP_parameter
carriage_line_control_cycle : Unknown (0.02s)
"""

Z3 output:
"""
Call_provers: command is: z3 -T:1 -smt2 sat.random_seed=42
  nlsat.randomize=false smt.random_seed=42

/tmp/why_235f6a_carriagemnlinemncontrolmnce-T-WP_parameter_carriage_line_control_cycle.smt2
Call_provers: exited with status 0
Call_provers: prover output:
timeout

Call_provers: model:
Call_provers:
carriage-line-control-ce.mlw Carriage_Line_Control WP_parameter
carriage_line_control_cycle : Timeout (1.02s)
"""

>From past discussion in this thread
(https://lists.gforge.inria.fr/pipermail/why3-club/2016-June/001364.html),
it seems that I'm stuck.

I tried, as Yannick told they are doing for SPARK, to use a specific
CVC4 driver with logic set to AUFLIRA but I don't get any specific error
message:
"""
Call_provers: command is: cvc4 --tlimit-per=10000 --lang=smt2

/tmp/why_729dbd_carriagemnlinemncontrolmnce-T-WP_parameter_carriage_line_control_cycle.smt2
Call_provers: exited with status 0
Call_provers: prover output:
unknown
(:reason-unknown incomplete)

Call_provers: model:
Call_provers:
carriage-line-control-ce.mlw Carriage_Line_Control WP_parameter
carriage_line_control_cycle : Unknown (0.02s)
"""

In case of CVC4 is used in AUFLIRA with non linear arithmetic, which
error message am I supposed to have? For now I don't really understand
why it says I'm using non linear arithmetic. In fact, I'm using only
"var+1" arithmetic operation but combined with if and pattern matching,
would if be the reason?

Best regards,
david



More information about the Why3-club mailing list