From 1bdababddf743ee1ee2a37809bfab33ff1dc63c6 Mon Sep 17 00:00:00 2001
From: Bruno Marre <bruno.marre@cea.fr>
Date: Thu, 30 May 2024 17:50:13 +0200
Subject: [PATCH] =?UTF-8?q?mouveaux=20benchs=20=C3=A0=20copier=20dans=20Un?=
 =?UTF-8?q?it=5Ftests/unsat/QF=5FFPNRA?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/unsat/sq_id_fp_nra_10_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_11_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_12_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_13_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_14_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_15_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_16_unsat.smt2 | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_17_unsat.smt2 | 21 +++++++++++++++++++
 tests/unsat/sq_id_fp_nra_1_unsat.smt2  | 28 ++++++++++++++++++++++++++
 tests/unsat/sq_id_fp_nra_2_unsat.smt2  | 26 ++++++++++++++++++++++++
 tests/unsat/sq_id_fp_nra_3_unsat.smt2  | 25 +++++++++++++++++++++++
 tests/unsat/sq_id_fp_nra_4_unsat.smt2  | 21 +++++++++++++++++++
 tests/unsat/sq_id_fp_nra_5_unsat.smt2  | 21 +++++++++++++++++++
 tests/unsat/sq_id_fp_nra_6_unsat.smt2  | 21 +++++++++++++++++++
 tests/unsat/sq_id_fp_nra_7_unsat.smt2  | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_8_unsat.smt2  | 20 ++++++++++++++++++
 tests/unsat/sq_id_fp_nra_9_unsat.smt2  | 20 ++++++++++++++++++
 17 files changed, 363 insertions(+)
 create mode 100644 tests/unsat/sq_id_fp_nra_10_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_11_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_12_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_13_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_14_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_15_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_16_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_17_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_1_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_2_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_3_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_4_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_5_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_6_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_7_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_8_unsat.smt2
 create mode 100644 tests/unsat/sq_id_fp_nra_9_unsat.smt2

diff --git a/tests/unsat/sq_id_fp_nra_10_unsat.smt2 b/tests/unsat/sq_id_fp_nra_10_unsat.smt2
new file mode 100644
index 000000000..f7423503a
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_10_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* 3.0 x x) (* 4.0 y y) (* 4.0 x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_11_unsat.smt2 b/tests/unsat/sq_id_fp_nra_11_unsat.smt2
new file mode 100644
index 000000000..d284b3b2f
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_11_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (+ (* (- 1.0) x x) (* (- 1.0) y y) (* (- 2.0) x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_12_unsat.smt2 b/tests/unsat/sq_id_fp_nra_12_unsat.smt2
new file mode 100644
index 000000000..dfb45a3aa
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_12_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (+ (* (- 1.0) x x) (* (- 1.0) y y) (* 2.0 x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_13_unsat.smt2 b/tests/unsat/sq_id_fp_nra_13_unsat.smt2
new file mode 100644
index 000000000..6682e098e
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_13_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* 4.0 x x) (* 3.0 x) 1.0))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_14_unsat.smt2 b/tests/unsat/sq_id_fp_nra_14_unsat.smt2
new file mode 100644
index 000000000..6682e098e
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_14_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* 4.0 x x) (* 3.0 x) 1.0))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_15_unsat.smt2 b/tests/unsat/sq_id_fp_nra_15_unsat.smt2
new file mode 100644
index 000000000..d5fcc6dba
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_15_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* (- 2.0) x) 1.0)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_16_unsat.smt2 b/tests/unsat/sq_id_fp_nra_16_unsat.smt2
new file mode 100644
index 000000000..04306425e
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_16_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* x x) x (/ 1.0 4.0)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_17_unsat.smt2 b/tests/unsat/sq_id_fp_nra_17_unsat.smt2
new file mode 100644
index 000000000..aaf4c1c35
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_17_unsat.smt2
@@ -0,0 +1,21 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) x (/ 1.0 4.0))))
+))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_1_unsat.smt2 b/tests/unsat/sq_id_fp_nra_1_unsat.smt2
new file mode 100644
index 000000000..61e8ff9ab
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_1_unsat.smt2
@@ -0,0 +1,28 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(define-fun s2 () Real
+  (+ (+ (+ (- (* (* 1.9 x) x)
+	      (* y y))
+	   (* (* 2.0 x) y))
+	(* (* 1.1 x) x))
+     (* (* 4.0 y) y)))
+
+(assert (not
+        (=> (and (<= (- 2.0) x 2.0) (<= (- 2.0) y 2.0)) (<= 0.0 s2 32.0))
+))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_2_unsat.smt2 b/tests/unsat/sq_id_fp_nra_2_unsat.smt2
new file mode 100644
index 000000000..711b2ee00
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_2_unsat.smt2
@@ -0,0 +1,26 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(define-fun s2r () Real
+  (+ (* (+ x y) (+ x y))
+     (* 2.0 x x)
+     (* 2.0 y y)))
+
+(assert (not
+        (=> (and (<= (- 2.0) x 2.0) (<= (- 2.0) y 2.0)) (<= 0.0 s2r 32.0))
+))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_3_unsat.smt2 b/tests/unsat/sq_id_fp_nra_3_unsat.smt2
new file mode 100644
index 000000000..307183440
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_3_unsat.smt2
@@ -0,0 +1,25 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+
+(define-fun s2 () Real
+  (+ (+ (+ (- (* (* 1.9 x) x)
+	      (* y y))
+	   (* (* 2.0 x) y))
+	(* (* 1.1 x) x))
+     (* (* 4.0 y) y)))
+
+(define-fun s2r () Real
+  (+ (* (+ x y) (+ x y))
+     (* 2.0 x x)
+     (* 2.0 y y)))
+
+(assert (not
+	(= s2 s2r)
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_4_unsat.smt2 b/tests/unsat/sq_id_fp_nra_4_unsat.smt2
new file mode 100644
index 000000000..fbb0baee4
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_4_unsat.smt2
@@ -0,0 +1,21 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(= (- (+ (* x x) (* y y)) (* 2.0 x y)) (* (- x y) (+ (- y) x)))
+))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_5_unsat.smt2 b/tests/unsat/sq_id_fp_nra_5_unsat.smt2
new file mode 100644
index 000000000..519728621
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_5_unsat.smt2
@@ -0,0 +1,21 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* y y) (* 2.0 x y))))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_6_unsat.smt2 b/tests/unsat/sq_id_fp_nra_6_unsat.smt2
new file mode 100644
index 000000000..6bb3c0a88
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_6_unsat.smt2
@@ -0,0 +1,21 @@
+
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* x x) (* y y) (* 2.0 x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_7_unsat.smt2 b/tests/unsat/sq_id_fp_nra_7_unsat.smt2
new file mode 100644
index 000000000..67679541f
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_7_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* y y) (* (- 2.0) x y))))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_8_unsat.smt2 b/tests/unsat/sq_id_fp_nra_8_unsat.smt2
new file mode 100644
index 000000000..abfaa4660
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_8_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(<= 0.0 (+ (* x x) (* y y) (* (- 2.0) x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_fp_nra_9_unsat.smt2 b/tests/unsat/sq_id_fp_nra_9_unsat.smt2
new file mode 100644
index 000000000..ccbdf5eb7
--- /dev/null
+++ b/tests/unsat/sq_id_fp_nra_9_unsat.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FPNRA)
+(set-info :category |Crafted from GATeL POs|)
+(set-info :status unsat)
+
+(declare-fun dx () Float64)
+(declare-fun dy () Float64)
+(define-fun x () Real
+  (fp.to_real dx))
+(define-fun y () Real
+  (fp.to_real dy))
+(define-fun isFinite ((F Float64)) Bool
+  (and (not (fp.isInfinite F))
+       (not (fp.isNaN F))))
+(assert (and (isFinite dx) (isFinite dy)))
+
+(assert (not
+	(>= 0.0 (- (+ (* 3.0 x x) (* 4.0 y y) (* 4.0 x y))))
+	))
+(check-sat)
-- 
GitLab