From dc8d92b8b90016b82f52c79b494c3536adba4793 Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Tue, 12 Feb 2019 10:34:27 +0100
Subject: [PATCH] example for issue #269, can't reproduce

---
 examples/bts/269_replace_under_if.mlw         |  10 ++++++++
 .../bts/269_replace_under_if/why3session.xml  |  23 ++++++++++++++++++
 .../bts/269_replace_under_if/why3shapes.gz    | Bin 0 -> 143 bytes
 3 files changed, 33 insertions(+)
 create mode 100644 examples/bts/269_replace_under_if.mlw
 create mode 100644 examples/bts/269_replace_under_if/why3session.xml
 create mode 100644 examples/bts/269_replace_under_if/why3shapes.gz

diff --git a/examples/bts/269_replace_under_if.mlw b/examples/bts/269_replace_under_if.mlw
new file mode 100644
index 000000000..2c4d39213
--- /dev/null
+++ b/examples/bts/269_replace_under_if.mlw
@@ -0,0 +1,10 @@
+
+use int.Int
+
+constant a : int
+
+constant b : int
+
+axiom H : a = b
+
+goal G : if a > 0 then true else false
diff --git a/examples/bts/269_replace_under_if/why3session.xml b/examples/bts/269_replace_under_if/why3session.xml
new file mode 100644
index 000000000..c1c7aa3a2
--- /dev/null
+++ b/examples/bts/269_replace_under_if/why3session.xml
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<file>
+<path name=".."/>
+<path name="269_replace_under_if.mlw"/>
+<theory name="Top">
+ <goal name="G">
+ <transf name="replace" arg1="a" arg2="b">
+  <goal name="G.0">
+  </goal>
+  <goal name="G.1" expl="equality hypothesis">
+  </goal>
+ </transf>
+ <transf name="rewrite" arg1="H">
+  <goal name="G.0">
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/bts/269_replace_under_if/why3shapes.gz b/examples/bts/269_replace_under_if/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..9ba073f554d6d7e1f5647ccb5c0b9f88763c8e5c
GIT binary patch
literal 143
zcmV;A0C4{wiwFP!00000|CNn94#F@DKzB}&Bc!ooI|JOsPGU6@;-dzM-kuIDjO_12
z6+JSur&=SRlX$n%nl-m2A&22p$IZt(TvTg3acqgj30X4~f&@K@q}&M>$Wng<I|TA3
xEC<_>(Jf|#vQROIjayL;{rS@Cn0r|F$9=AS8{0Q<R#p4|_yN`u)Hl=s001B+J(~ak

literal 0
HcmV?d00001

-- 
2.24.1