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

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


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, CVC4 always answer "non linear arith"!

Any idea on what is going on?

Here is CVC4 (1.4) output I obtain:
"""
$ why3 prove -C why3.config -L . --get-ce -P cvc4 --debug call_prover
counter_example_test.mlw
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_40c6c1_counter_example_test-T-WP_parameter_f.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)
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter f : Unknown (0.00s)
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_37b13f_counter_example_test-T-WP_parameter_g1.smt2
Call_provers: exited with status 1
Call_provers: prover output:
SmtEngine: turning off produce-models because unsupported for nonlinear
arith
unsat
(error "Can't get-info :reason-unknown when the last result wasn't
unknown!")
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter g1 : Valid (0.00s)
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_d010eb_counter_example_test-T-WP_parameter_g2.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)
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter g2 : Unknown (0.00s)
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_42913c_counter_example_test-T-WP_parameter_h.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)
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter h : Unknown (0.00s)
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_d2ac12_counter_example_test-T-WP_parameter_k.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)
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter k : Unknown (0.00s)
Call_provers: command is: /home/student/.opam/4.02.3/lib/why3/why3-cpulimit
  11 1000 -s cvc4 --tlimit-per=10000 --lang=smt2
  /tmp/why_f63fd3_counter_example_test-T-WP_parameter_k2.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)
why3cpulimit time : 0.000000 s

Call_provers: model:
Call_provers:
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
"""

Best regards,
david

-------------- next part --------------
module Counter_example

  use import int.Int

  type s_t = {
    x : int;
    y : int;
  }

  let f (x "model" : int) : int
  ensures { result > 0 }
  = x+x

  let g1 (x : int) : int
  ensures { result = x + x }
  = x+x

  let g2 (x "model" : int) : int
  ensures { result > 0 }
  = g1 x

  let h (x "model" : int) : int
  returns { r -> r > 0 }
  = g1 x

  let k (s "model" : s_t) : s_t
  returns { r -> r.x > 0 }
  returns { r -> r.y > 0 } (* FIXME: why counter example is s.x = 0? *)
  = { x = g1 s.x; y = g1 s.y }

  let k2 (s "model" : s_t) : s_t
  returns { r -> r.x > 0 }
  returns { r -> "model_vc" r.y > 0 }
  = { x = g1 s.x; y = g1 s.y }

end

(*
$ why3 prove -C why3.config -P z3 --get-ce -a split_goal_wp counter_example_test.mlw
counter_example_test.mlw Counter_example WP_parameter f : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 10:
x = 0
counter_example_test.mlw Counter_example WP_parameter g1 : Valid (0.00s)
counter_example_test.mlw Counter_example WP_parameter g2 : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 18:
x = 0
counter_example_test.mlw Counter_example WP_parameter h : Unknown (0.01s)
Counter-example model:File counter_example_test.mlw:
Line 22:
x = 0
counter_example_test.mlw Counter_example WP_parameter k : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 26:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 26:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
Counter-example model:File counter_example_test.mlw:
Line 31:
s.x = 0
counter_example_test.mlw Counter_example WP_parameter k2 : Unknown (0.00s)
Counter-example model:File /home/student/.opam/4.02.3/share/why3/theories/int.why:
Line 17:
s.y = 0File counter_example_test.mlw:
Line 31:
s.y = 0
*)


More information about the Why3-club mailing list