Commit 80f7df9e authored by Sylvain Dailler's avatar Sylvain Dailler

Adding test for issue #79.

parent d8017e38
module Soundness
use import int.Int
use HighOrd
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (\x. f0 x y z) <-> y = z
meta rewrite prop A
(* compute_specified should not solve this goal.
0 = 0 was added so that compute_specified progress on this goal even when
not unsound.
*)
lemma Fail : 0 = 0 /\ p (\x. f0 x x x)
lemma Absurd : false
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../79_compute_unsound.mlw">
<theory name="Soundness" sum="aa1c41b51a76f536179c52b8dcf8a473">
<goal name="A" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Fail">
<transf name="compute_specified" >
<goal name="Fail.0">
</goal>
</transf>
</goal>
<goal name="Absurd" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -49,7 +49,7 @@ module Soundness
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (\x. f0 x y z) <-> y = z
meta rewrite prop A
lemma Fail : p (\x. f0 x x x)
lemma Fail : 0 = 0 /\ p (\x. f0 x x x)
lemma Absurd : false
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment