Commit 88049731 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following:

commit 43dc8073
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Fri May 13 16:31:12 2022 -0700

    Moved non-linear benchmarks to UFFPDTNIRA.
parent f6c38837
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 16777216) i)
(<= i 16777216)))
(define-fun same_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float32) (x Float32)
(y Float32)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float32)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float32)))))
(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
(declare-sort float__ 0)
(declare-fun user_eq (float__ float__) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE1 (Float32) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Float32)
(declare-const dummy float__)
(declare-datatypes ((float____ref 0))
(((float____refqtmk (float____content float__)))))
(define-fun float____ref_float____content__projection ((a float____ref)) float__
(float____content a))
(define-fun dynamic_invariant ((temp___expr_60 Float32)
(temp___is_init_56 Bool) (temp___skip_constant_57 Bool)
(temp___do_toplevel_58 Bool)
(temp___do_typ_inv_59 Bool)) Bool (=>
(or (= temp___is_init_56 true)
(fp.leq (fp.neg (fp #b0 #b11111110 #b11111111111111111111111)) (fp #b0 #b11111110 #b11111111111111111111111)))
(fp.isFinite32 temp___expr_60)))
(declare-const attr__ATTRIBUTE_ADDRESS Int)
(declare-const distance_to_target Float32)
(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
(assert
;; defqtvc
;; File "flight_manager.adb", line 9, characters 0-0
(not
(forall ((f Float32) (f1 Float32) (f2 Float32))
(=> (= f1 f)
(=> (dynamic_invariant f true false true true)
(=> (dynamic_invariant distance_to_target true false true true)
(=>
(exists ((spark__branch Bool))
(and
(= spark__branch (ite (fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
true false))
(ite (= spark__branch true)
(let ((o (fp.mul RNE f distance_to_target)))
(and (fp.isFinite32 o)
(= f2 (fp.div RNE o (fp #b0 #b10000010 #b01000000000000000000000)))))
(= f2 f))))
(=>
(fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
(fp.eq f2 (fp.div RNE (fp.mul RNE f1 distance_to_target) (fp #b0 #b10000010 #b01000000000000000000000)))))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 16777216) i)
(<= i 16777216)))
(define-fun same_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float32) (x Float32)
(y Float32)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float32)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float32)))))
(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
(declare-sort float__ 0)
(declare-fun user_eq (float__ float__) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE1 (Float32) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Float32)
(declare-const dummy float__)
(declare-datatypes ((float____ref 0))
(((float____refqtmk (float____content float__)))))
(define-fun float____ref_float____content__projection ((a float____ref)) float__
(float____content a))
(define-fun dynamic_invariant ((temp___expr_60 Float32)
(temp___is_init_56 Bool) (temp___skip_constant_57 Bool)
(temp___do_toplevel_58 Bool)
(temp___do_typ_inv_59 Bool)) Bool (=>
(or (= temp___is_init_56 true)
(fp.leq (fp.neg (fp #b0 #b11111110 #b11111111111111111111111)) (fp #b0 #b11111110 #b11111111111111111111111)))
(fp.isFinite32 temp___expr_60)))
(declare-const attr__ATTRIBUTE_ADDRESS Int)
(declare-const distance_to_target Float32)
(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
(assert
;; defqtvc
;; File "flight_manager.adb", line 9, characters 0-0
(not
(forall ((f Float32) (f1 Float32))
(=> (dynamic_invariant f true false true true)
(=> (dynamic_invariant distance_to_target true false true true)
(=>
(exists ((spark__branch Bool))
(and
(= spark__branch (ite (fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
true false))
(ite (= spark__branch true)
(let ((o (fp.mul RNE f distance_to_target)))
(and (fp.isFinite32 o)
(= f1 (fp.div RNE o (fp #b0 #b10000010 #b01000000000000000000000)))))
(= f1 f))))
(=>
(fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
(fp.isFinite32 (fp.mul RNE f distance_to_target)))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 16777216) i)
(<= i 16777216)))
(define-fun same_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float32) (x Float32)
(y Float32)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float32)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float32)))))
(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
(declare-sort float__ 0)
(declare-fun user_eq (float__ float__) Bool)
(declare-fun attr__ATTRIBUTE_IMAGE1 (Float32) us_image)
(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Float32)
(declare-const dummy float__)
(declare-datatypes ((float____ref 0))
(((float____refqtmk (float____content float__)))))
(define-fun float____ref_float____content__projection ((a float____ref)) float__
(float____content a))
(define-fun dynamic_invariant ((temp___expr_60 Float32)
(temp___is_init_56 Bool) (temp___skip_constant_57 Bool)
(temp___do_toplevel_58 Bool)
(temp___do_typ_inv_59 Bool)) Bool (=>
(or (= temp___is_init_56 true)
(fp.leq (fp.neg (fp #b0 #b11111110 #b11111111111111111111111)) (fp #b0 #b11111110 #b11111111111111111111111)))
(fp.isFinite32 temp___expr_60)))
(declare-const attr__ATTRIBUTE_ADDRESS Int)
(declare-const distance_to_target Float32)
(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
(assert
;; defqtvc
;; File "flight_manager.adb", line 9, characters 0-0
(not
(forall ((f Float32) (f1 Float32))
(=> (dynamic_invariant f true false true true)
(=> (dynamic_invariant distance_to_target true false true true)
(=>
(exists ((spark__branch Bool))
(and
(= spark__branch (ite (fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
true false))
(ite (= spark__branch true)
(let ((o (fp.mul RNE f distance_to_target)))
(and (fp.isFinite32 o)
(= f1 (fp.div RNE o (fp #b0 #b10000010 #b01000000000000000000000)))))
(= f1 f))))
(=>
(fp.lt distance_to_target (fp #b0 #b10000010 #b01000000000000000000000))
(=> (fp.isFinite32 (fp.mul RNE f distance_to_target))
(not (fp.isZero (fp #b0 #b10000010 #b01000000000000000000000)))))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic UFFPDTLIRA)
(set-info :source |
Generated by: AdaCore
Generated on: 2020-03-06
Generator: SPARK
Application: Program verification for Ada
Target solver: CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-sort us_private 0)
(declare-fun private__bool_eq (us_private us_private) Bool)
(declare-const us_null_ext__ us_private)
(declare-sort us_type_of_heap 0)
(declare-datatypes ((us_type_of_heap__ref 0))
(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
(declare-sort us_image 0)
(declare-datatypes ((int__ref 0))
(((int__refqtmk (int__content Int)))))
(declare-datatypes ((bool__ref 0))
(((bool__refqtmk (bool__content Bool)))))
(declare-datatypes ((us_fixed__ref 0))
(((us_fixed__refqtmk (us_fixed__content Int)))))
(declare-datatypes ((real__ref 0))
(((real__refqtmk (real__content Real)))))
(declare-datatypes ((us_private__ref 0))
(((us_private__refqtmk (us_private__content us_private)))))
(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
a))
(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
(define-fun us_private__ref___projection ((a us_private__ref)) us_private
(us_private__content a))
(declare-fun pow2 (Int) Int)
(define-fun is_plus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isPositive x)))
(define-fun is_minus_infinity ((x Float32)) Bool (and (fp.isInfinite x)
(fp.isNegative x)))
(define-fun is_plus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isPositive x)))
(define-fun is_minus_zero ((x Float32)) Bool (and (fp.isZero x)
(fp.isNegative x)))
(declare-const max_int Int)
(define-fun in_int_range ((i Int)) Bool (and (<= (- max_int) i)
(<= i max_int)))
(define-fun in_safe_int_range ((i Int)) Bool (and (<= (- 16777216) i)
(<= i 16777216)))
(define-fun same_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isPositive y))
(and (fp.isNegative x) (fp.isNegative y))))
(define-fun diff_sign ((x Float32)
(y Float32)) Bool (or (and (fp.isPositive x) (fp.isNegative y))
(and (fp.isNegative x) (fp.isPositive y))))
(define-fun product_sign ((z Float32) (x Float32)
(y Float32)) Bool (and (=> (same_sign x y) (fp.isPositive z))
(=> (diff_sign x y) (fp.isNegative z))))
(define-fun sqr ((x Real)) Real (* x x))
(declare-fun sqrt1 (Real) Real)
(define-fun same_sign_real ((x Float32)
(r Real)) Bool (or (and (fp.isPositive x) (< 0.0 r))
(and (fp.isNegative x) (< r 0.0))))
(declare-datatypes ((t__ref 0))
(((t__refqtmk (t__content Float32)))))
(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)