Squashed commit of the following:

commit be6dff75
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Fri Apr 24 22:44:51 2020 -0700

    Move benchmarks from pending repository.

20190906-CLEARSY/0004/00003.smt2

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