test/regress/regress2/quantifiers/cee-event-wrong-sat.smt2

   1 ; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
   2 ; COMMAND-LINE: --full-saturate-quant --ee-mode=central
   3 ; EXPECT: unsat
   4 (set-logic ALL)
   5 (set-info :status unsat)
   6 (declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T))))
   7 (declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int)))))
   8 (declare-sort |T@[Int]$Value| 0)
   9 (declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int)))))
  10 (declare-sort b 0)
  11 (declare-sort l 0)
  12 (declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l)))))
  13 (declare-fun $EmptyValueArray () T@R)
  14 (declare-fun m (T@$Value) |T@[Int]$Value|)
  15 (declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool)
  16 (declare-fun sel (|T@[Int]$Value| Int) T@$Value)
  17 (declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
  18 (assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1))))
  19 (assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1))))
  20 (declare-fun $LibraAccount_T_type_value () T@$TypeValue)
  21 (declare-fun s (l T@$Location) T@$Value)
  22 (declare-fun $Event_EventHandleGenerator_counter () Int)
  23 (declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
  24 (assert (= 0 (|l#R| $EmptyValueArray)))
  25 (assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
  26 (assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
  27 (declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
  28 (declare-fun $m@@0 () T@M)
  29 (declare-fun $abort_flag@2 () Bool)
  30 (declare-fun $m@3 () T@M)
  31 (declare-fun mv () T@$TypeValue)
  32 (declare-fun inline$$MoveToRaw$0$a@0 () Int)
  33 (declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b)
  34 (assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1)))))
  35 (declare-fun inline$$MoveToRaw$0$l@1 () T@$Location)
  36 (declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l)
  37 (assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1))))
  38 (assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1))))
  39 (declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value)
  40 (declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value)
  41 (declare-fun i () T@$Value)
  42 (assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3))))))))))))))))))))))))))))
  43 (check-sat)