summaryrefslogtreecommitdiff
path: root/test/regress/regress1/fmf/agree466.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/fmf/agree466.smt2')
-rw-r--r--test/regress/regress1/fmf/agree466.smt2474
1 files changed, 474 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/agree466.smt2 b/test/regress/regress1/fmf/agree466.smt2
new file mode 100644
index 000000000..d17a663c6
--- /dev/null
+++ b/test/regress/regress1/fmf/agree466.smt2
@@ -0,0 +1,474 @@
+; COMMAND-LINE: --finite-model-find --lang=smt2.5
+; EXPECT: sat
+; 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback