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

Move benchmarks from pending repository.

parent 39d410b3
(set-info :smt-lib-version 2.6)
(set-logic QF_UFNRA)
(set-info :source |
Generated by: David Deharbe, CLEARSY
Generated on: 2019-09-06
Generator: bxml;pog;pog2smt (Atelier B)
Application: Event-B
Target solver: CVC4, Z3
|)
(set-info :license "https://creativecommons.org/licenses/by-nc/4.0/")
(set-info :category "academic")
(set-info :status sat)
; Prelude
(declare-fun |*i| (Real Real) Real)
(declare-fun |+i| (Real Real) Real)
(declare-fun |-i| (Real Real) Real)
(declare-fun idiv (Real Real) Real)
(declare-fun modulo (Real Real) Real)
(declare-fun |<i| (Real Real) Bool)
(declare-fun |<=i| (Real Real) Bool)
(declare-fun |>i| (Real Real) Bool)
(declare-fun |>=i| (Real Real) Bool)
(declare-fun iuminus (Real) Real)
(declare-fun TRUE () Real)
(declare-fun FALSE () Real)
(assert (not (= TRUE FALSE)))
(declare-fun empty () Real)
(declare-fun bool (Bool) Real)
(declare-fun BOOL () Real)
(declare-fun INT () Real)
(declare-fun INTEGER () Real)
(declare-fun NAT () Real)
(declare-fun NAT1 () Real)
(declare-fun NATURAL () Real)
(declare-fun NATURAL1 () Real)
(declare-fun FLOAT () Real)
(declare-fun MaxInt () Real)
(declare-fun MinInt () Real)
(declare-fun |STRING| () Real)
(declare-fun REAL () Real)
(declare-fun set_prod (Real Real) Real)
(declare-fun set_diff (Real Real) Real)
(declare-fun mapplet (Real Real) Real)
(declare-fun |**i| (Real Real) Real)
(declare-fun |**r| (Real Real) Real)
(declare-fun |+->| (Real Real) Real)
(declare-fun |+->>| (Real Real) Real)
(declare-fun |-->| (Real Real) Real)
(declare-fun |-->>| (Real Real) Real)
(declare-fun |<->| (Real Real) Real)
(declare-fun |>+>| (Real Real) Real)
(declare-fun |>->| (Real Real) Real)
(declare-fun |>+>>| (Real Real) Real)
(declare-fun |>->>| (Real Real) Real)
(declare-fun |->| (Real Real) Real)
(declare-fun interval (Real Real) Real)
(declare-fun composition (Real Real) Real)
(declare-fun binary_inter (Real Real) Real)
(declare-fun restriction_head (Real Real) Real)
(declare-fun semicolon (Real Real) Real)
(declare-fun |<+| (Real Real) Real)
(declare-fun |<-| (Real Real) Real)
(declare-fun domain_subtraction (Real Real) Real)
(declare-fun domain_restriction (Real Real) Real)
(declare-fun |><| (Real Real) Real)
(declare-fun parallel_product (Real Real) Real)
(declare-fun binary_union (Real Real) Real)
(declare-fun restriction_tail (Real Real) Real)
(declare-fun concatenate (Real Real) Real)
(declare-fun range_restriction (Real Real) Real)
(declare-fun range_subtraction (Real Real) Real)
(declare-fun image (Real Real) Real)
(declare-fun apply (Real Real) Real)
(declare-fun prj1 (Real Real) Real)
(declare-fun prj2 (Real Real) Real)
(declare-fun iterate (Real Real) Real)
(declare-fun |const| (Real Real) Real)
(declare-fun rank (Real Real) Real)
(declare-fun father (Real Real) Real)
(declare-fun subtree (Real Real) Real)
(declare-fun arity (Real Real) Real)
(declare-fun |+f| (Real Real) Real)
(declare-fun |-f| (Real Real) Real)
(declare-fun |*f| (Real Real) Real)
(declare-fun |fdiv| (Real Real) Real)
(declare-fun tbin (Real Real Real) Real)
(declare-fun son (Real Real Real) Real)
(declare-fun mem (Real Real) Bool)
(declare-fun subset (Real Real) Bool)
(declare-fun strict_subset (Real Real) Bool)
(declare-fun |<=f| (Real Real) Bool)
(declare-fun |<f| (Real Real) Bool)
(declare-fun |>=f| (Real Real) Bool)
(declare-fun |>f| (Real Real) Bool)
(declare-fun imax (Real) Real)
(declare-fun imin (Real) Real)
(declare-fun rmax (Real) Real)
(declare-fun rmin (Real) Real)
(declare-fun card (Real) Real)
(declare-fun dom (Real) Real)
(declare-fun ran (Real) Real)
(declare-fun POW (Real) Real)
(declare-fun POW1 (Real) Real)
(declare-fun FIN (Real) Real)
(declare-fun FIN1 (Real) Real)
(declare-fun union (Real) Real)
(declare-fun inter (Real) Real)
(declare-fun seq (Real) Real)
(declare-fun seq1 (Real) Real)
(declare-fun iseq (Real) Real)
(declare-fun iseq1 (Real) Real)
(declare-fun inverse (Real) Real)
(declare-fun size (Real) Real)
(declare-fun perm (Real) Real)
(declare-fun first (Real) Real)
(declare-fun last (Real) Real)
(declare-fun id (Real) Real)
(declare-fun closure (Real) Real)
(declare-fun closure1 (Real) Real)
(declare-fun tail (Real) Real)
(declare-fun front (Real) Real)
(declare-fun reverse (Real) Real)
(declare-fun rev (Real) Real)
(declare-fun conc (Real) Real)
(declare-fun succ (Real) Real)
(declare-fun pred (Real) Real)
(declare-fun rel (Real) Real)
(declare-fun fnc (Real) Real)
(declare-fun real (Real) Real)
(declare-fun floor (Real) Real)
(declare-fun ceiling (Real) Real)
(declare-fun tree (Real) Real)
(declare-fun btree (Real) Real)
(declare-fun top (Real) Real)
(declare-fun sons (Real) Real)
(declare-fun prefix (Real) Real)
(declare-fun postfix (Real) Real)
(declare-fun sizet (Real) Real)
(declare-fun mirror (Real) Real)
(declare-fun left (Real) Real)
(declare-fun right (Real) Real)
(declare-fun infix (Real) Real)
(declare-fun ubin (Real) Real)
(declare-fun SEQ (Real) Real)
(declare-fun SET (Real) Real)
; Opaque formulas
(declare-fun g_s0_1 () Real)
(declare-fun g_s1_0 () Real)
(declare-fun g_s2_2 () Real)
(declare-fun g_s3_3 () Real)
(declare-fun g_s4_4 () Real)
(declare-fun g_s5_5 () Real)
(declare-fun g_s6_6 () Real)
(declare-fun g_s7_7 () Real)
(declare-fun g_s8_8 () Real)
(declare-fun e10 () Real)
(declare-fun e12 () Real)
(declare-fun e9 () Real)
(declare-fun e11 () Real)
(declare-fun e16 () Real)
(declare-fun e15 () Real)
(declare-fun e14 () Real)
(declare-fun e13 () Real)
; Defines
(define-fun |def_B definitions| () Bool (and (= NAT (interval 0.0 MaxInt)) (= INT (interval MinInt MaxInt))))
(define-fun |def_ctx| () Bool true)
(define-fun |def_seext| () Bool true)
(define-fun |def_lprp| () Bool (and (mem g_s0_1 (|-->| g_s1_0 (POW g_s1_0))) (mem g_s2_2 (|-->| g_s1_0 (POW g_s1_0))) (mem g_s3_3 (|-->| g_s1_0 (POW g_s1_0))) (mem g_s4_4 (|-->| g_s1_0 (POW g_s1_0))) (mem g_s5_5 (|-->| (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s6_6 (|-->| (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s7_7 (|-->| (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s8_8 (|-->| (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (= g_s0_1 e9) (= g_s2_2 e10) (= g_s3_3 e11) (= g_s4_4 e12) (= g_s5_5 e13) (= g_s6_6 e14) (= g_s7_7 e15) (= g_s8_8 e16)))
(define-fun |def_inprp| () Bool true)
(define-fun |def_inext| () Bool true)
(define-fun |def_inv| () Bool true)
(define-fun |def_ass| () Bool (= (dom g_s7_7) (set_prod g_s1_0 g_s1_0)))
(define-fun |def_cst| () Bool true)
(define-fun |def_sets| () Bool true)
; PO group 0
(assert |def_B definitions|)
(assert |def_ctx|)
(assert |def_cst|)
(assert |def_lprp|)
(assert |def_inprp|)
(assert |def_inext|)
(assert |def_seext|)
(assert |def_inv|)
; PO 1 in group 0
(assert (not (= (dom g_s7_7) (set_prod g_s1_0 g_s1_0))))
(check-sat)
(exit)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment