mouveaux benchs à copier dans Unit_tests/unsat/QF_FPNRA

tests/unsat/sq_id_fp_nra_10_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_11_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_12_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_13_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_14_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_15_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_16_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_17_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_1_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_2_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_3_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_4_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_5_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_6_unsat.smt2

+
+(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)

tests/unsat/sq_id_fp_nra_7_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_8_unsat.smt2

+(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)

tests/unsat/sq_id_fp_nra_9_unsat.smt2

+(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)