From d03756044a8156d29dbb002ae38d849ad7cb4d4a Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 25 May 2023 18:07:30 +0200
Subject: [PATCH] [tests] Promote tests following rebase

---
 tests/pyrat.t      | 52 ++++++++++++++++++++++++++++++++++++----------
 tests/pyrat_onnx.t | 12 ++++++++---
 2 files changed, 50 insertions(+), 14 deletions(-)

diff --git a/tests/pyrat.t b/tests/pyrat.t
index 8de49de..da619dd 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -41,7 +41,7 @@ Test verify
   >   use int.Int
   >   use interpretation.Vector
   >   use interpretation.NeuralNetwork
-  >
+  > 
   >   constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
   > 
   >   goal H:
@@ -52,16 +52,46 @@ Test verify
   > end
   > EOF
   [caisar][INFO] Task sent to prover:
-  0.0 < x0
-  x0 < 0.5
-  0.5 < x1
-  x1 < 1.0
-  (0.0 < y0 or 0.5 < y0) and 0.0 < y1 and y1 < 0.5
+  0.0 <= x0
+  x0 <= 0.5
+  0.5 <= x1
+  x1 <= 1.0
+  (0.0 <  y0 or 0.5 <  y0)
+  
+  [caisar][INFO] Task sent to prover:
+  0.0 <= x0
+  x0 <= 0.5
+  0.5 <= x1
+  x1 <= 1.0
+  0.0 <  y1
+  
+  [caisar][INFO] Task sent to prover:
+  0.0 <= x0
+  x0 <= 0.5
+  0.5 <= x1
+  x1 <= 1.0
+  y1 <  0.5
+  
+  [caisar][INFO] Task sent to prover:
+  0.375 <= x0
+  x0 <= 0.75
+  0.5 <= x1
+  x1 <= 1.0
+  (0.0 <  y0 or 0.5 <  y0)
+  
+  [caisar][INFO] Task sent to prover:
+  0.375 <= x0
+  x0 <= 0.75
+  0.5 <= x1
+  x1 <= 1.0
+  0.0 <  y1
+  
   [caisar][INFO] Task sent to prover:
-  0.375 < x0
-  x0 < 0.75
-  0.5 < x1
-  x1 < 1.0
-  (0.0 < y0 or 0.5 < y0) and 0.0 < y1 and y1 < 0.5
+  0.375 <= x0
+  x0 <= 0.75
+  0.5 <= x1
+  x1 <= 1.0
+  y1 <  0.5
+  
   [caisar][INFO] Verification results for theory 'PyRAT_oracle'
   [caisar] Goal H: Unknown ()
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 8b65e02..d02b661 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -24,8 +24,14 @@ Test verify
   > end
   > EOF
   [caisar][INFO] Task sent to prover:
-  0.0 < x0
-  x0 < 0.5
-  0.0 < y0 and y0 < 0.5
+  0.0 <= x0
+  x0 <= 0.5
+  0.0 <  y0
+  
+  [caisar][INFO] Task sent to prover:
+  0.0 <= x0
+  x0 <= 0.5
+  y0 <  0.5
+  
   [caisar][INFO] Verification results for theory 'PyRAT_ONNX'
   [caisar] Goal G: Unknown ()
-- 
GitLab