diff --git a/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_10_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_10_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..f7423503ac437f489330d47ffb64457577464a30
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_11_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_11_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d284b3b2fb438c3b9aaba2e22d00f1f82bb450b6
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_12_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_12_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..dfb45a3aa14b16c4168fe595b5c76dd2568d4f0f
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_13_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_13_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..6682e098ebdb52578d58240388ca1fa73e10531a
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_14_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_14_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..6682e098ebdb52578d58240388ca1fa73e10531a
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_15_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_15_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d5fcc6dbae8aea1cd78c26b8bfe9b0f2b765801b
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_16_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_16_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..04306425eff5d03a141fb0ddb936065e8b46d1fe
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_17_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_17_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..aaf4c1c3585bc758508741658cea8d8468a8867d
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_1_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_1_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..61e8ff9abcb05914ea773031e24503c9728a3d5b
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_2_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_2_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..711b2ee00ede47add8c66742dc0942042f9216e5
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_3_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_3_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..30718344006d5bfb637c9ebae1f82051f6698992
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_4_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_4_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..fbb0baee4ef1925f47e2a7b60c060d42f6895225
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_5_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_5_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..5197286210b7aa83e9bb0a3f74557f7ac2410ee1
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_6_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_6_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..6bb3c0a887c61a295464b30fd2af9c8b1224e166
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_7_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_7_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..67679541f479d065faa0ae79df1240f3bedc1b5e
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_8_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_8_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..abfaa4660469eb3c973d843194fb78ede0b7f620
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_9_unsat.smt2 b/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_9_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..ccbdf5eb7e5a1b7deb4914b6213119240bb43862
--- /dev/null
+++ b/UnitTests/unsat/QF_FPNRA/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)