From 7fbc34e635f933e5df1ae7e83c5fd36c6f769db0 Mon Sep 17 00:00:00 2001
From: Bruno Marre <bruno.marre@cea.fr>
Date: Thu, 30 May 2024 18:48:12 +0200
Subject: [PATCH] encore des benchs

---
 tests/unsat/sq_id_fp_nra_3_unsat.smt2  | 14 +++++++++++---
 tests/unsat/sq_id_fp_nra_3_unsat.smt2~ | 25 +++++++++++++++++++++++++
 tests/unsat/sq_id_nra_10_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_11_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_12_unsat.smat2   | 12 ++++++++++++
 tests/unsat/sq_id_nra_13_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_14_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_15_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_16_unsat.smt2    | 12 ++++++++++++
 tests/unsat/sq_id_nra_1_unsat.smt2     | 20 ++++++++++++++++++++
 tests/unsat/sq_id_nra_2_unsat.smt2     | 18 ++++++++++++++++++
 tests/unsat/sq_id_nra_3_unsat.smt2     | 25 +++++++++++++++++++++++++
 tests/unsat/sq_id_nra_4_unsat.smt2     | 13 +++++++++++++
 tests/unsat/sq_id_nra_5_unsat.smt2     | 13 +++++++++++++
 tests/unsat/sq_id_nra_6_unsat.smt2     | 13 +++++++++++++
 tests/unsat/sq_id_nra_7_unsat.smt2     | 12 ++++++++++++
 tests/unsat/sq_id_nra_8_unsat.smt2     | 12 ++++++++++++
 tests/unsat/sq_id_nra_9_unsat.smt2     | 12 ++++++++++++
 18 files changed, 258 insertions(+), 3 deletions(-)
 create mode 100644 tests/unsat/sq_id_fp_nra_3_unsat.smt2~
 create mode 100644 tests/unsat/sq_id_nra_10_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_11_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_12_unsat.smat2
 create mode 100644 tests/unsat/sq_id_nra_13_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_14_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_15_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_16_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_1_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_2_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_3_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_4_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_5_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_6_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_7_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_8_unsat.smt2
 create mode 100644 tests/unsat/sq_id_nra_9_unsat.smt2

diff --git a/tests/unsat/sq_id_fp_nra_3_unsat.smt2 b/tests/unsat/sq_id_fp_nra_3_unsat.smt2
index 307183440..02c87c8fe 100644
--- a/tests/unsat/sq_id_fp_nra_3_unsat.smt2
+++ b/tests/unsat/sq_id_fp_nra_3_unsat.smt2
@@ -1,11 +1,19 @@
 
 (set-info :smt-lib-version 2.6)
-(set-logic QF_NRA)
+(set-logic QF_FPNRA)
 (set-info :category |Crafted from GATeL POs|)
 (set-info :status unsat)
 
-(declare-fun x () Real)
-(declare-fun y () Real)
+(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)
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_nra_10_unsat.smt2 b/tests/unsat/sq_id_nra_10_unsat.smt2
new file mode 100644
index 000000000..b93c0cb70
--- /dev/null
+++ b/tests/unsat/sq_id_nra_10_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(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_nra_11_unsat.smt2 b/tests/unsat/sq_id_nra_11_unsat.smt2
new file mode 100644
index 000000000..f4ca782ef
--- /dev/null
+++ b/tests/unsat/sq_id_nra_11_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(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_nra_12_unsat.smat2 b/tests/unsat/sq_id_nra_12_unsat.smat2
new file mode 100644
index 000000000..c05955562
--- /dev/null
+++ b/tests/unsat/sq_id_nra_12_unsat.smat2
@@ -0,0 +1,12 @@
+(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)
+
+(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_nra_13_unsat.smt2 b/tests/unsat/sq_id_nra_13_unsat.smt2
new file mode 100644
index 000000000..beba7da32
--- /dev/null
+++ b/tests/unsat/sq_id_nra_13_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(<= 0.0 (+ (* 4.0 x x) (* 3.0 x) 1.0))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_14_unsat.smt2 b/tests/unsat/sq_id_nra_14_unsat.smt2
new file mode 100644
index 000000000..beba7da32
--- /dev/null
+++ b/tests/unsat/sq_id_nra_14_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(<= 0.0 (+ (* 4.0 x x) (* 3.0 x) 1.0))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_15_unsat.smt2 b/tests/unsat/sq_id_nra_15_unsat.smt2
new file mode 100644
index 000000000..629138ad6
--- /dev/null
+++ b/tests/unsat/sq_id_nra_15_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* (- 2.0) x) 1.0)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_16_unsat.smt2 b/tests/unsat/sq_id_nra_16_unsat.smt2
new file mode 100644
index 000000000..4eadc4967
--- /dev/null
+++ b/tests/unsat/sq_id_nra_16_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(<= 0.0 (+ (* x x) x (/ 1.0 4.0)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_1_unsat.smt2 b/tests/unsat/sq_id_nra_1_unsat.smt2
new file mode 100644
index 000000000..87de4d646
--- /dev/null
+++ b/tests/unsat/sq_id_nra_1_unsat.smt2
@@ -0,0 +1,20 @@
+
+(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)))
+
+(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_nra_2_unsat.smt2 b/tests/unsat/sq_id_nra_2_unsat.smt2
new file mode 100644
index 000000000..33e83e589
--- /dev/null
+++ b/tests/unsat/sq_id_nra_2_unsat.smt2
@@ -0,0 +1,18 @@
+
+(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 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_nra_3_unsat.smt2 b/tests/unsat/sq_id_nra_3_unsat.smt2
new file mode 100644
index 000000000..307183440
--- /dev/null
+++ b/tests/unsat/sq_id_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_nra_4_unsat.smt2 b/tests/unsat/sq_id_nra_4_unsat.smt2
new file mode 100644
index 000000000..c1dee8727
--- /dev/null
+++ b/tests/unsat/sq_id_nra_4_unsat.smt2
@@ -0,0 +1,13 @@
+
+(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)
+
+(assert (not
+	(= (- (+ (* x x) (* y y)) (* 2.0 x y)) (* (- x y) (+ (- y) x)))
+))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_5_unsat.smt2 b/tests/unsat/sq_id_nra_5_unsat.smt2
new file mode 100644
index 000000000..b06024beb
--- /dev/null
+++ b/tests/unsat/sq_id_nra_5_unsat.smt2
@@ -0,0 +1,13 @@
+
+(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)
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* y y) (* 2.0 x y))))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_6_unsat.smt2 b/tests/unsat/sq_id_nra_6_unsat.smt2
new file mode 100644
index 000000000..5d84c9c80
--- /dev/null
+++ b/tests/unsat/sq_id_nra_6_unsat.smt2
@@ -0,0 +1,13 @@
+
+(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)
+
+(assert (not
+	(<= 0.0 (+ (* x x) (* y y) (* 2.0 x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_7_unsat.smt2 b/tests/unsat/sq_id_nra_7_unsat.smt2
new file mode 100644
index 000000000..a5b42331b
--- /dev/null
+++ b/tests/unsat/sq_id_nra_7_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(>= 0.0 (- (+ (* x x) (* y y) (* (- 2.0) x y))))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_8_unsat.smt2 b/tests/unsat/sq_id_nra_8_unsat.smt2
new file mode 100644
index 000000000..d646ed5ba
--- /dev/null
+++ b/tests/unsat/sq_id_nra_8_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(<= 0.0 (+ (* x x) (* y y) (* (- 2.0) x y)))
+	))
+(check-sat)
diff --git a/tests/unsat/sq_id_nra_9_unsat.smt2 b/tests/unsat/sq_id_nra_9_unsat.smt2
new file mode 100644
index 000000000..c1b5fb1e2
--- /dev/null
+++ b/tests/unsat/sq_id_nra_9_unsat.smt2
@@ -0,0 +1,12 @@
+(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)
+
+(assert (not
+	(>= 0.0 (- (+ (* 3.0 x x) (* 4.0 y y) (* 4.0 x y))))
+	))
+(check-sat)
-- 
GitLab