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 _______________________________________________ Why3-club mailing list [email protected] http://lists.gforge.inria.fr/mailman/listinfo/why3-club
