summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf/agree467.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/fmf/agree467.smt2')
-rw-r--r--test/regress/regress0/fmf/agree467.smt2341
1 files changed, 0 insertions, 341 deletions
diff --git a/test/regress/regress0/fmf/agree467.smt2 b/test/regress/regress0/fmf/agree467.smt2
deleted file mode 100644
index 07180cf4f..000000000
--- a/test/regress/regress0/fmf/agree467.smt2
+++ /dev/null
@@ -1,341 +0,0 @@
-; COMMAND-LINE: --finite-model-find --lang=smt2.5
-; EXPECT: unsat
-; Preamble --------------
-(set-logic ALL_SUPPORTED)
-(set-info :status unsat)
-(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 init_done () node_set$type)
-(declare-fun crashed () Nodes$t$type)
-(declare-fun comp_done () node_set$type)
-(declare-fun chosen () (Array node$type BOOL))
-(declare-fun recv_done () node_pair_set$type)
-(declare-fun phase () phase_state$type)
-(declare-fun clean () clean_state$type)
-(declare-fun global_state () state_set$type)
-(declare-fun messages () (Array node$type message_set$type))
-(declare-fun deliver_message () failure_pattern$type)
-(declare-fun crashing () Nodes$t$type)
-(declare-fun round () Int)
-(declare-fun send_done () node_pair_set$type)
-
-; Asserts --------------
-(declare-fun mk_array_8 () (Array node$type BOOL))
-;mk_array_8_def :
-(assert (forall ((mk_array_8_index node$type)) (= (select mk_array_8
- mk_array_8_index) Falsity)))
-(declare-fun mk_array_9 () (Array node$type message_set$type))
-;mk_array_9_def :
-(assert (forall ((mk_array_9_index node$type)) (= (select mk_array_9
- mk_array_9_index) null_message_set)))
-(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and
- (and
- (=
- clean
- before)
- (=
- global_state
- null_state_set))
- (=
- messages
- mk_array_9))
- (= deliver_message
- full_node_pair_set))
- (= comp_done
- empty_node_set))
- (= recv_done empty_node_pair_set))
- (= send_done empty_node_pair_set))
- (= init_done empty_node_set))
- (= phase init_phase)) (= crashing
- Nodes$empty))
- (= crashed Nodes$empty)) (= round 0)) (= chosen
- mk_array_8))
- (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))))))))
-
-(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback