From b146b42103678fb93ec91df7651d465f6cb0e256 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 17 May 2021 21:25:51 +0200
Subject: [PATCH] Add ACAS XU property #1 in why3 syntax.

---
 acasxu.why | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 acasxu.why

diff --git a/acasxu.why b/acasxu.why
new file mode 100644
index 0000000..33c6ee6
--- /dev/null
+++ b/acasxu.why
@@ -0,0 +1,22 @@
+theory ACAS_XU_P1
+
+  use real.Real
+
+  constant x0:real
+  axiom x0: 0.6 <= x0 <= 0.6798577687
+  
+  constant x1:real
+  axiom x1: -0.5 <= x1 <= 0.5
+  
+  constant x2:real
+  axiom x2: -0.5 <= x2 <= 0.5
+  
+  constant x3:real
+  axiom x3: 0.45 <= x3 <= 0.5
+  
+  constant x4:real
+  axiom x4: -0.5 <= x4 <= -0.45
+  
+  goal P1: forall y0:real. y0 <= 3.9911256459
+
+end
-- 
GitLab