tests for first-order matching

tests/demo-itp.mlw

 
+module ApplyRewrite
+
+  use import int.Int
+
+  (* Use apply H require some cases of quantifications in first_order_matching *)
+  goal g: (forall y. exists x. x <= y /\ y = 0) -> forall x. exists y. y <= x /\ x = 0
+
+
+end
+
+
 module TestCEX
 
   use import int.Int

tests/demo-itp/why3session.xml

@@ -10,6 +10,12 @@
 <prover id="5" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="6" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../demo-itp.mlw">
+<theory name="ApplyRewrite" proved="true" sum="06c28a672d2fbb0de6998078f2cfe895">
+ <goal name="g" proved="true">
+ <transf name="apply" proved="true" arg1="H">
+ </transf>
+ </goal>
+</theory>
 <theory name="TestCEX" sum="55ceea8b24a88c1829a53af2c814f1a6">
  <goal name="g">
  <proof prover="2" timelimit="5"><result status="unknown" time="0.00"/></proof>