Commit 0579ac10 authored by MARCHE Claude's avatar MARCHE Claude

Fix problem with gappa substitution: subtitute modulo alpha-renaming to

ignore labels
parent 80dea17f
......@@ -88,10 +88,13 @@ theory GappaEq2
goal G1 : value result - value q1 * value q2 <= 0x1.p-52
goal G2 : forall q:double. q = result ->
value q - value q1 * value q2 <= 0x1.p-52
constant q : double
axiom H3 : q = result
goal G2 : value q - value q1 * value q2 <= 0x1.p-52
goal G3 : value q - value q1 * value q2 <= 0x1.p-52
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session
name="gappa/why3session.xml">
<prover
......@@ -193,8 +193,8 @@
shape="ainfix &lt;=ainfix -avaluearesultainfix *avalueaq1avalueaq2c0x1.p-52">
<proof
prover="0"
timelimit="5"
memlimit="1000"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -203,15 +203,32 @@
<goal
name="G2"
locfile="gappa/../gappa.why"
loclnum="95" loccnumb="7" loccnume="9"
sum="c95bf026f3487c9617ff54cc4bf4902d"
loclnum="91" loccnumb="7" loccnume="9"
sum="584bf8809239d409f578d27a534924c5"
proved="true"
expanded="true"
shape="ainfix &lt;=ainfix -avalueV0ainfix *avalueaq1avalueaq2c0x1.p-52Iainfix =V0aresultF">
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="G3"
locfile="gappa/../gappa.why"
loclnum="98" loccnumb="7" loccnume="9"
sum="9469b135d544f3a9e1746b6492709b0f"
proved="false"
expanded="true"
shape="ainfix &lt;=ainfix -avalueaqainfix *avalueaq1avalueaq2c0x1.p-52">
<proof
prover="0"
timelimit="5"
memlimit="1000"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
......
......@@ -202,7 +202,7 @@ let rec fmla_cond_subst filter f =
for j = 0 to subl - 1 do
if j <> i then
let (f, s) = subf.(j) in
subf.(j) <- (t_replace t1 t2 f, s);
subf.(j) <- (t_replace_alpha t1 t2 f, s);
done in
let (f, s) = subf.(i) in
match f.t_node with
......
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