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
index 30718344006d5bfb637c9ebae1f82051f6698992..02c87c8fe555d2c80f59a482c39d197376494540 100644
--- a/UnitTests/unsat/QF_FPNRA/sq_id_fp_nra_3_unsat.smt2
+++ b/UnitTests/unsat/QF_FPNRA/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/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_NRA/sq_id_nra_10_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_10_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..b93c0cb70a7ca6c8dedfa9707b82c7b7b084cf28
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_11_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_11_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..f4ca782ef0552b3420418f544b250c5cc64ef9ed
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_12_unsat.smat2 b/UnitTests/unsat/QF_NRA/sq_id_nra_12_unsat.smat2
new file mode 100644
index 0000000000000000000000000000000000000000..c059555626d26d921990a869b13661f0e76b1c9c
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_13_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_13_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..beba7da3297d47bf1cf7588c1ee3b7b96ca1eb54
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_14_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_14_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..beba7da3297d47bf1cf7588c1ee3b7b96ca1eb54
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_15_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_15_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..629138ad67c480a033e96fa2cbbbbd298698fe48
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_16_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_16_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..4eadc4967669188d1e7021e43e214206d2a33ed4
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_1_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_1_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..87de4d64625d6eef7b41906fd61245f45c01c515
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_2_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_2_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..33e83e5890b1f234131afd247ee6d26977b4c996
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_3_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_3_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..30718344006d5bfb637c9ebae1f82051f6698992
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_4_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_4_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..c1dee8727d348f32f8fadf2eddb28c2e7ced5f7d
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_5_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_5_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..b06024beb9a3c9797588067180a33510eb38bfcf
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_6_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_6_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..5d84c9c80d004e52013452b8b5e3f910f9296b5b
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_7_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_7_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..a5b42331bb4b6feb96723b42ade12314ec8d8349
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_8_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_8_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..d646ed5baf1d2d2aaee2aa8fa8fdf10cf3af9f2f
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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/UnitTests/unsat/QF_NRA/sq_id_nra_9_unsat.smt2 b/UnitTests/unsat/QF_NRA/sq_id_nra_9_unsat.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..c1b5fb1e2af6982444d2a888842e0cbe4fdbfab2
--- /dev/null
+++ b/UnitTests/unsat/QF_NRA/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)