; COMMAND-LINE: --finite-model-find
; EXPECT: sat
; EXIT: 10
; Preamble  --------------
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-datatypes () ((UNIT (Unit))))
(declare-datatypes () ((BOOL (Truth) (Falsity))))

; Decls     --------------
(declare-sort node$type 0)
(declare-sort value$type 0)
(define-sort Nodes$elem$type () node$type)
(declare-sort Nodes$t$type 0)
(declare-fun Nodes$empty () Nodes$t$type)
(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL)
(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$cardinality (Nodes$t$type) Int)
(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type)
(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL)
;Nodes$disjoint_empty :
(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth)))
;Nodes$disjoint_comm :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b) 
                                                    (Nodes$disjoint b a))))
;Nodes$mem_empty :
(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty) 
                                           Truth))))
;Nodes$mem_add :
(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) 
        (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s) 
                                                          Truth)) Truth 
                                         Falsity))))
;Nodes$mem_remove :
(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type)) 
        (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (= 
                                                                    (Nodes$mem 
                                                                    x s) 
                                                                    Truth)) 
                                            Truth Falsity))))
;Nodes$mem_union1 :
(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a) 
                                                           Truth) (forall 
                                                                  ((b Nodes$t$type)) 
                                                                  (= 
                                                                  (Nodes$mem 
                                                                  x (Nodes$union 
                                                                    a b)) 
                                                                  Truth)))))
;Nodes$mem_union2 :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b) 
                                                    (Nodes$union b a))))
;Nodes$mem_union3 :
(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type)) 
        (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a) 
                                                          Truth) (= (Nodes$mem 
                                                                    x b) 
                                                                 Truth)))))
;Nodes$mem_union4 :
(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a)))
;Nodes$mem_union5 :
(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a)))
;Nodes$empty_union :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b) 
                                                        Nodes$empty) 
                                                    (= a Nodes$empty))))
;Nodes$card_empty :
(assert (= (Nodes$cardinality Nodes$empty) 0))
;Nodes$card_zero :
(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (= 
                                                                   s 
                                                                   Nodes$empty))))
;Nodes$card_non_negative :
(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0)))
;Nodes$card_add :
(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality 
                                                          (Nodes$add x s)) 
                                                       (ite (= (Nodes$mem 
                                                               x s) Truth) 
                                                       (Nodes$cardinality 
                                                       s) (+ (Nodes$cardinality 
                                                             s) 1)))))
;Nodes$card_remove :
(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality 
                                                          (Nodes$remove x s)) 
                                                       (ite (= (Nodes$mem 
                                                               x s) Truth) (- 
                                                       (Nodes$cardinality 
                                                       s) 1) (Nodes$cardinality 
                                                             s)))))
;Nodes$card_union :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint 
                                                           a b) Truth) 
                                                    (= (Nodes$cardinality 
                                                       (Nodes$union a b)) (+ 
                                                    (Nodes$cardinality 
                                                    a) (Nodes$cardinality b))))))
(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL)
;Nodes$eq_is_equality :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b) 
                                                    (ite (= a b) Truth 
                                                    Falsity))))
;Nodes$equal1 :
(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type)) 
                                                        (= (Nodes$mem x a) 
                                                        (Nodes$mem x b))) 
                                                    (= (Nodes$eq a b) 
                                                    Truth))))
(define-sort Values$elem$type () value$type)
(declare-sort Values$t$type 0)
(declare-fun Values$empty () Values$t$type)
(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL)
(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type)
(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type)
(declare-fun Values$cardinality (Values$t$type) Int)
(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type)
(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL)
;Values$disjoint_empty :
(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty) 
                                    Truth)))
;Values$disjoint_comm :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint 
                                                         a b) (Values$disjoint 
                                                              b a))))
;Values$mem_empty :
(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty) 
                                            Truth))))
;Values$mem_add :
(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) 
        (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem 
                                                               x s) Truth)) 
                                           Truth Falsity))))
;Values$mem_remove :
(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type)) 
        (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y)) 
                                                   (= (Values$mem x s) 
                                                   Truth)) Truth Falsity))))
;Values$mem_union1 :
(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem 
                                                                x a) 
                                                             Truth) (forall 
                                                                    (
                                                                    (b Values$t$type)) 
                                                                    (= 
                                                                    (Values$mem 
                                                                    x 
                                                                    (Values$union 
                                                                    a b)) 
                                                                    Truth)))))
;Values$mem_union2 :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b) 
                                                      (Values$union b a))))
;Values$mem_union3 :
(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type)) 
        (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem 
                                                               x a) Truth) 
                                                        (= (Values$mem x b) 
                                                        Truth)))))
;Values$mem_union4 :
(assert (forall ((a Values$t$type)) (= (Values$union a a) a)))
;Values$mem_union5 :
(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a)))
;Values$empty_union :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union 
                                                             a b) Values$empty) 
                                                      (= a Values$empty))))
;Values$card_empty :
(assert (= (Values$cardinality Values$empty) 0))
;Values$card_zero :
(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0) 
                                    (= s Values$empty))))
;Values$card_non_negative :
(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0)))
;Values$card_add :
(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality 
                                                            (Values$add x s)) 
                                                         (ite (= (Values$mem 
                                                                 x s) 
                                                              Truth) 
                                                         (Values$cardinality 
                                                         s) (+ (Values$cardinality 
                                                               s) 1)))))
;Values$card_remove :
(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality 
                                                            (Values$remove 
                                                            x s)) (ite 
                                                                  (= 
                                                                  (Values$mem 
                                                                  x s) 
                                                                  Truth) (- 
                                                                  (Values$cardinality 
                                                                  s) 
                                                                  1) 
                                                                  (Values$cardinality 
                                                                  s)))))
;Values$card_union :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint 
                                                             a b) Truth) 
                                                      (= (Values$cardinality 
                                                         (Values$union a b)) (+ 
                                                      (Values$cardinality 
                                                      a) (Values$cardinality 
                                                         b))))))
(declare-fun Values$eq (Values$t$type Values$t$type) BOOL)
;Values$eq_is_equality :
(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b) 
                                                      (ite (= a b) Truth 
                                                      Falsity))))
;Values$equal1 :
(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type)) 
                                                          (= (Values$mem x a) 
                                                          (Values$mem 
                                                          x b))) (= (Values$eq 
                                                                    a b) 
                                                                 Truth))))
(define-sort node_set$type () (Array node$type BOOL))
(declare-fun mk_array_1 () (Array node$type BOOL))
;mk_array_1_def :
(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1 
                                                  mk_array_1_index) Falsity)))
(define-fun empty_node_set () node_set$type mk_array_1)
(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL)))
(declare-fun mk_array_2 () (Array node$type BOOL))
;mk_array_2_def :
(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2 
                                                  mk_array_2_index) Falsity)))
(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL)))
;mk_array_3_def :
(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3 
                                                  mk_array_3_index) mk_array_2)))
(define-fun empty_node_pair_set () node_pair_set$type mk_array_3)
(declare-fun mk_array_4 () (Array node$type BOOL))
;mk_array_4_def :
(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4 
                                                  mk_array_4_index) Truth)))
(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL)))
;mk_array_5_def :
(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5 
                                                  mk_array_5_index) mk_array_4)))
(define-fun full_node_pair_set () node_pair_set$type mk_array_5)
(declare-fun input () (Array node$type value$type))
(declare-fun t () Int)
;positive_bound :
(assert (> t 0))
(define-sort message$type () Values$t$type)
(define-sort message_set$type () (Array node$type message$type))
(define-sort state$type () Values$t$type)
(define-sort state_set$type () (Array node$type state$type))
(define-fun null_message () message$type Values$empty)
(declare-fun mk_array_6 () (Array node$type message$type))
;mk_array_6_def :
(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6 
                                                  mk_array_6_index) null_message)))
(define-fun null_message_set () message_set$type mk_array_6)
(define-fun null_state () state$type Values$empty)
(declare-fun mk_array_7 () (Array node$type state$type))
;mk_array_7_def :
(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 
                                                  mk_array_7_index) null_state)))
(define-fun null_state_set () state_set$type mk_array_7)
(declare-fun choose (Values$t$type) value$type)
;choosen_value :
(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem 
                                                                    (choose 
                                                                    vals) 
                                                                    vals) 
                                                                 Truth))))
(define-sort failure_pattern$type () node_pair_set$type)
(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL 
(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth))) 
Truth Falsity))
(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL 
(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth))) 
Truth Falsity))
(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase))))
(declare-datatypes () ((clean_state$type (before) (active) (after))))

; Var Decls --------------
(declare-fun my_compute$result$1 () state$type)
(declare-fun output$1 () (Array node$type value$type))
(declare-fun comp_done () node_set$type)
(declare-fun compute$can_decide$0$1 () BOOL)
(declare-fun chosen () (Array node$type BOOL))
(declare-fun recv_done () node_pair_set$type)
(declare-fun output () (Array node$type value$type))
(declare-fun phase () phase_state$type)
(declare-fun global_state () state_set$type)
(declare-fun my_decide$result$1 () value$type)
(declare-fun round () Int)
(declare-fun compute$n () node$type)
(declare-fun send_done () node_pair_set$type)
(declare-fun my_can_decide$result$1 () BOOL)
(declare-fun chosen$1 () (Array node$type BOOL))
(declare-fun comp_done$1 () node_set$type)
(declare-fun global_state$1 () state_set$type)

; Asserts   --------------
(assert (not (=> (forall ((n node$type)) (=> 
                                                                    (and 
                                                                    (= 
                                                                    (select 
                                                                    chosen 
                                                                    n) 
                                                                    Truth) 
                                                                    (= 
                                                                    round (+ 
                                                                    t 
                                                                    1))) 
                                                                    (and 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    send_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth)) 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    recv_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth))))) 
                                        (=> (= phase comp_phase) (=> 
                                                                 (not 
                                                                 (= (select 
                                                                    comp_done 
                                                                    compute$n) 
                                                                 Truth)) 
                                                                 (=> 
                                                                 (= my_compute$result$1 
                                                                 (select 
                                                                 global_state 
                                                                 compute$n)) 
                                                                 (=> 
                                                                 (= global_state$1 
                                                                 (store 
                                                                 global_state 
                                                                 compute$n 
                                                                 my_compute$result$1)) 
                                                                 (=> 
                                                                 (= my_can_decide$result$1 
                                                                 (ite 
                                                                 (= round (+ 
                                                                 t 1)) 
                                                                 Truth 
                                                                 Falsity)) 
                                                                 (=> 
                                                                 (= compute$can_decide$0$1 
                                                                 my_can_decide$result$1) 
                                                                 (= (ite 
                                                                    (= 
                                                                    compute$can_decide$0$1 
                                                                    Truth) 
                                                                    (ite 
                                                                    (=> 
                                                                    (= 
                                                                    my_decide$result$1 
                                                                    (choose 
                                                                    (select 
                                                                    global_state$1 
                                                                    compute$n))) 
                                                                    (=> 
                                                                    (= 
                                                                    output$1 
                                                                    (store 
                                                                    output 
                                                                    compute$n 
                                                                    my_decide$result$1)) 
                                                                    (=> 
                                                                    (= 
                                                                    chosen$1 
                                                                    (store 
                                                                    chosen 
                                                                    compute$n 
                                                                    Truth)) 
                                                                    (=> 
                                                                    (= 
                                                                    comp_done$1 
                                                                    (store 
                                                                    comp_done 
                                                                    compute$n 
                                                                    Truth)) 
                                                                    (forall 
                                                                    (
                                                                    (n node$type)) 
                                                                    (=> 
                                                                    (and 
                                                                    (= 
                                                                    (select 
                                                                    chosen$1 
                                                                    n) 
                                                                    Truth) 
                                                                    (= 
                                                                    round (+ 
                                                                    t 
                                                                    1))) 
                                                                    (and 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    send_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth)) 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    recv_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth))))))))) 
                                                                    Truth 
                                                                    Falsity) 
                                                                    (ite 
                                                                    (=> 
                                                                    (= 
                                                                    comp_done$1 
                                                                    (store 
                                                                    comp_done 
                                                                    compute$n 
                                                                    Truth)) 
                                                                    (forall 
                                                                    (
                                                                    (n node$type)) 
                                                                    (=> 
                                                                    (and 
                                                                    (= 
                                                                    (select 
                                                                    chosen 
                                                                    n) 
                                                                    Truth) 
                                                                    (= 
                                                                    round (+ 
                                                                    t 
                                                                    1))) 
                                                                    (and 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    send_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth)) 
                                                                    (forall 
                                                                    (
                                                                    (n node$type) (m node$type)) 
                                                                    (= 
                                                                    (select 
                                                                    (select 
                                                                    recv_done 
                                                                    n) 
                                                                    m) 
                                                                    Truth)))))) 
                                                                    Truth 
                                                                    Falsity)) 
                                                                 Truth))))))))))
                           
(check-sat)