Skip to content
Snippets Groups Projects
Commit 7fbc34e6 authored by Bruno Marre's avatar Bruno Marre Committed by Christophe Junke
Browse files

encore des benchs

parent 46fe8c00
No related branches found
No related tags found
1 merge request!55Update and fix tests
Showing
with 258 additions and 3 deletions
(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)
......
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
(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)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment