ppc-all.rkt

#lang racket

(require "../lang.rkt")

(provide (all-defined-out) (all-from-out "../lang.rkt"))

(define-litmus-test test/ppc/aclwdrr000
  (((W z 1)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr001
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr002
  (((W y 1)
    (F sync)
    (W x 1))
   ((W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr003
  (((W z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr004
  (((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1))
   ((W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr005
  (((W z 1)
    (F sync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr006
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr007
  (((W y 1)
    (F lwsync)
    (W x 1))
   ((W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr008
  (((W z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr009
  (((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1))
   ((W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr010
  (((R y 1)
    (F lwsync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr011
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr012
  (((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr013
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr014
  (((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr015
  (((W z 1)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr016
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr017
  (((W y 1)
    (F sync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr018
  (((W z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr019
  (((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr020
  (((W y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R x 1))
   ((W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr021
  (((W z 1)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr022
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/aclwdrr023
  (((W y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr024
  (((W a 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr025
  (((W z 1)
    (F sync)
    (W z 2))
   ((R z 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr026
  (((W a 1)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr027
  (((W z 1)
    (F lwsync)
    (W z 2))
   ((R z 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr028
  (((W z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr029
  (((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr030
  (((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr031
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr032
  (((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr033
  (((W y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwdrr034
  (((W z 1)
    (F sync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr035
  (((W z 1)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr036
  (((W y 1)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr037
  (((W a 1)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr038
  (((W z 1)
    (F lwsync)
    (W z 2))
   ((R z 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr039
  (((W z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr040
  (((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0)))
  #:post ((y 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr041
  (((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwdrr042
  (((W y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwsrr000
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R y 2)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/aclwsrr001
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2))
   ((R y 2)
    (F lwsync)
    (R y 2)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/aclwsrr002
  (((R x 1)
    (F lwsync)
    (R x 1)
    (R y 0 (2)))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)
    (R x 0 (2)))
   ((W x 1)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/aclwsrr003
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R x 1)
    (R y 0 (2)))
   ((W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwsrr004
  (((W y 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwsrr005
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwsrr006
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/aclwsrr007
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)
    (R x 0 (2))))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww000
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (W x 1 (0))))
  #:post ((x 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww001
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (W x 1 (0))))
  #:post ((x 2) (z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww002
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww003
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (R x 0 (0))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww004
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (R z 1 (0))))
  #:post ((y 2) (z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww005
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (R x 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww006
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1)))
  #:post ((y 2) (z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww007
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (W x 1 (0))))
  #:post ((y 2) (x 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww008
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww009
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (R x 0 (0))))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww010
  (((W y 2)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R y 1 (0))))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww011
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R x 0)))
  #:post ((y 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww012
  (((W y 2)
    (F lwsync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww013
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww014
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww015
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (R x 0 (0))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww016
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (R z 1 (0))))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww017
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (R x 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww018
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww019
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R x 0 (0))))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww020
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (R x 0 (0))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww021
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (R z 1 (0))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww022
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (R x 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww023
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww024
  (((W y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R y 1 (0))))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww025
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R x 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww026
  (((W y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwdww027
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R x 0)))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww028
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((R a 1)
    (F lwsync)
    (R x 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww029
  (((W z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/bclwdww030
  (((W y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/bclwsww000
  (((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (R x 0 (0))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/lwdwr020
  (((W y 1)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (R y 0)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/lwswr000
  (((W x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (R x 2)
    (R y 0 (2)))
   ((W y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (R y 2)
    (R x 0 (2))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/lwswr001
  (((W x 1)
    (F lwsync)
    (R x 1)
    (R y 0 (2)))
   ((W y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (R y 2)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/lwswr002
  (((W x 1)
    (F lwsync)
    (R x 1)
    (R y 0 (2)))
   ((W y 1)
    (F lwsync)
    (R y 1)
    (R x 0 (2))))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/lwswr003
  (((W x 1)
    (F lwsync)
    (R x 1)
    (R y 0 (2)))
   ((W y 1)
    (F lwsync)
    (R y 1)
    (R z 0 (2)))
   ((W z 1)
    (F lwsync)
    (R z 1)
    (R x 0 (2))))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podrr000
  (((W y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podrr001
  (((W a 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr002
  (((W z 1)
    (F sync)
    (W z 2))
   ((R z 2)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr003
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr004
  (((W a 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr005
  (((W z 1)
    (F sync)
    (W z 2))
   ((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr006
  (((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr007
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr008
  (((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr009
  (((W y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0)))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr010
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrr011
  (((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrw000
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrw001
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)))
  #:post ((a 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrw002
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrw003
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrw004
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)))
  #:post ((b 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr000
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W z 1)
    (R z 1)))
  #:post ((z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr001
  (((W c 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W z 1)
    (R z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W c 1)
    (R c 1)))
  #:post ((c 2) (z 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr002
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((y 2) (b 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr003
  (((W c 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)
    (R y 1)
    (R z 0 (2)))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W c 1)
    (R c 1)))
  #:post ((c 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr004
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr005
  (((W a 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr006
  (((W b 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr007
  (((W b 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((x 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr008
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr009
  (((W c 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)
    (R y 1)
    (W z 1 (2)))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W c 1)
    (R c 1)))
  #:post ((c 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr010
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((y 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr011
  (((W a 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (x 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr012
  (((W b 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((y 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr013
  (((W b 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((y 2) (x 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr014
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((y 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr015
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr016
  (((W b 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr017
  (((W b 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((x 2) (b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr018
  (((W b 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W b 1)
    (R b 1)))
  #:post ((b 2))
  #:allowed PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr019
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)
    (R y 1)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr020
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr021
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr022
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr023
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)
    (R x 0 (2))))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr024
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)
    (R a 0 (2)))
   ((W a 1)
    (F sync)
    (W b 1))
   ((R b 1)
    (W c 1)
    (R c 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr025
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)
    (R a 0 (2)))
   ((W a 1)
    (F sync)
    (W b 1))
   ((R b 1)
    (W c 1)
    (R c 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr026
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr027
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr028
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr029
  (((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr030
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr031
  (((W a 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr032
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr033
  (((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr034
  (((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr035
  (((W a 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr036
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr037
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr038
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr039
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr040
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr041
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr042
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)
    (W a 1 (2)))
   ((W a 2)
    (F sync)
    (W b 1))
   ((R b 1)
    (W c 1)
    (R c 1)
    (W x 1 (2))))
  #:post ((a 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr043
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr044
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr045
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr046
  (((W z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr047
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr048
  (((W a 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr049
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr050
  (((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr051
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (W x 1 (2))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr052
  (((W a 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (x 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr053
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((y 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr054
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((y 2) (x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr055
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr056
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr057
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2) (z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr058
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1)
    (R z 1)))
  #:post ((z 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr059
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr060
  (((W a 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr061
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr062
  (((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr063
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr064
  (((W a 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr065
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr066
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr067
  (((W a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1)
    (R a 1)))
  #:post ((a 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr068
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (R x 0 (2))))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podrwposwr069
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (W b 1)
    (R b 1)
    (W x 1 (2))))
  #:post ((x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/podwr000
  (((W y 1)
    (R x 0))
   ((W x 1)
    (R y 0)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podwr001
  (((W z 1)
    (R x 0))
   ((W x 1)
    (R y 0))
   ((W y 1)
    (R z 0)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podww000
  (((W y 2)
    (W x 1))
   ((W x 2)
    (W y 1)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/podww001
  (((W z 2)
    (W x 1))
   ((W x 2)
    (W y 1))
   ((W y 2)
    (W z 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/posrr000
  (((W y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (R x 1)
    (R y 0 (1))
    (R y 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr001
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1)
    (R z 0 (1))
    (R z 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr002
  (((W y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0))
    (R y 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr004
  (((W z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0))
    (R z 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr006
  (((W a 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0))
    (R a 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr007
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr008
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1)
    (R x 0 (1))))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr009
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr010
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr011
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1)
    (R x 0 (1))))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr012
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/posrr013
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((R a 1)
    (R a 1)
    (R x 0 (1))))
  #:allowed vacuous)

(define-litmus-test test/ppc/rfe000
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (W x 1 (0))))
  #:allowed vacuous)

(define-litmus-test test/ppc/rfe001
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (W z 1 (0)))
   ((R z 1)
    (W x 1 (0))))
  #:allowed vacuous)

(define-litmus-test test/ppc/rfe002
  (((R x 2)
    (W y 1 (0)))
   ((R y 1)
    (W x 1 (0)))
   ((W x 2)))
  #:post ((x 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/rfe003
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (R x 0 (0)))
   ((W x 1)))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/rfe004
  (((R x 2)
    (W y 1 (0)))
   ((W y 2))
   ((R y 2)
    (W x 1 (0)))
   ((W x 2)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/rfe005
  (((R x 1)
    (W y 1 (0)))
   ((W y 2))
   ((R y 2)
    (R x 0 (0)))
   ((W x 1)))
  #:post ((y 2))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/rfe006
  (((R x 1)
    (R y 0 (0)))
   ((W y 1))
   ((R y 1)
    (R x 0 (0)))
   ((W x 1)))
  #:allowed PPCherd PPCalglave vacuous)

(define-litmus-test test/ppc/rfi000
  (((W x 1)
    (R x 1)
    (R y 0 (1)))
   ((W y 1)
    (R y 1)
    (R x 0 (1))))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/rfi001
  (((W x 2)
    (R x 2)
    (R y 0 (1)))
   ((W y 1)
    (R y 1)
    (W x 1 (1))))
  #:post ((x 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/rfi002
  (((W x 2)
    (R x 2)
    (W y 1 (1)))
   ((W y 2)
    (R y 2)
    (W x 1 (1))))
  #:post ((y 2) (x 2))
  #:allowed PPCherd PPChw PPCalglave vacuous)

(define-litmus-test test/ppc/safe000
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe001
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe002
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe003
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe004
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe005
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe006
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe007
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe008
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe009
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe010
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe011
  (((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe012
  (((R x 1)
    (W y 1 (0)))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe013
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe014
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe015
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe016
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe017
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe018
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe019
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe020
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe021
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe022
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe023
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe024
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe025
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe026
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe027
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe028
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe029
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe030
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe031
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe032
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe033
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe034
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe035
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0)))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe036
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe037
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe038
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe039
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe040
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe041
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe042
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe043
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe044
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe045
  (((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe046
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe047
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe048
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe049
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe050
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe051
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe052
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe053
  (((R y 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe054
  (((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1))
   ((W x 2)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe055
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe056
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe057
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe058
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe059
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe060
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe061
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe062
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe063
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe064
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe065
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe066
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe067
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe068
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe069
  (((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe070
  (((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe071
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe072
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe073
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe074
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe075
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe076
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe077
  (((W x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe078
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe079
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe080
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe081
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe082
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe083
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe084
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe085
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe086
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe087
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe088
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe089
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe090
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe091
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe092
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe093
  (((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1))
   ((W x 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe094
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe095
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe096
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe097
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe098
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe099
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe100
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe101
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe102
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe103
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe104
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe105
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe106
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe107
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe108
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe109
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe110
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe111
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe112
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe113
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe114
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe115
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe116
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe117
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe118
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe119
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe120
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe121
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe122
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe123
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe124
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe125
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe126
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe127
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe128
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe129
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe130
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe131
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe132
  (((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe133
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe134
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe135
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe136
  (((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe137
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe138
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe139
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe140
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe141
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe142
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe143
  (((R y 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe144
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe145
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe146
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe147
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe148
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe149
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe150
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe151
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe152
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe153
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe154
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe155
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe156
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe157
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe158
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe159
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe160
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe161
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe162
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe163
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe164
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe165
  (((W x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe166
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe167
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe168
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe169
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe170
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe171
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe172
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe173
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe174
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2) (x 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe175
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe176
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe177
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe178
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe179
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe180
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe181
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe182
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe183
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe184
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe185
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe186
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe187
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe188
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe189
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed PPCherd vacuous)

(define-litmus-test test/ppc/safe190
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe191
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe192
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe193
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe194
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe195
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe196
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe197
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe198
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe199
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe200
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe201
  (((R z 2)
    (F sync)
    (W x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe202
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe203
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe204
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe205
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe206
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe207
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe208
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe209
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe210
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe211
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe212
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe213
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe214
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe215
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe216
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe217
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe218
  (((R y 2)
    (F sync)
    (W x 1))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe219
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe220
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0))
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe221
  (((R x 1)
    (W y 1 (0))
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe222
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0))
    (W z 2))
   ((R z 2)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe223
  (((R x 1)
    (R y 0 (0)))
   ((W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe224
  (((R x 1)
    (R x 1 (0)))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe225
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe226
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe227
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe228
  (((W x 1)
    (F sync)
    (R x 1))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe229
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe230
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe231
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe232
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe233
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe234
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe235
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe236
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe237
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0))
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe238
  (((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe239
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0))
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe240
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe241
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe242
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe243
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe244
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe245
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe246
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W y 2 (0)))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe247
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W y 2 (0)))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe248
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe249
  (((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe250
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe251
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe252
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe253
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe254
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe255
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe256
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe257
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe258
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe259
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe260
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe261
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe262
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe263
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe264
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe265
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe266
  (((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe267
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe268
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe269
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe270
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe271
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe272
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe273
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe274
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe275
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe276
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe277
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe278
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe279
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe280
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe281
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe282
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe283
  (((R x 1)
    (W y 1 (0))
    (W y 2))
   ((R y 2)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2) (y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe284
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0))
   ((W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe285
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe286
  (((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe287
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe288
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe289
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe290
  (((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (R x 0)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe291
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F sync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe292
  (((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe293
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe294
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe295
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe296
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1))
   ((W a 2)
    (F lwsync)
    (W x 1)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe297
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0))
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe298
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0))
    (W z 2)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe299
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (W z 1 (0))
    (W z 2)))
  #:post ((y 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe300
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0))
    (W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe301
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0))
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe302
  (((R a 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0))
    (W a 2)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe303
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0))
    (W z 2)))
  #:post ((x 2) (z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe304
  (((R a 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (W a 1 (0))
    (W a 2)))
  #:post ((a 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe305
  (((R y 2)
    (R x 0 (0)))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe306
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe307
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (R x 0)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe308
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe309
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe310
  (((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe311
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe312
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe313
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe314
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe315
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe316
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (R x 0)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe317
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe318
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe319
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe320
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe321
  (((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe322
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe323
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (R x 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe324
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe325
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe326
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (R y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe327
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe328
  (((R z 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe329
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe330
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe331
  (((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe332
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe333
  (((R z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe334
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe335
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe336
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0)))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe337
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (R x 0)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe338
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe339
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe340
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F sync)
    (R x 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe341
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (R z 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe342
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0)))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe343
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R a 0 (0)))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe344
  (((R x 1)
    (R x 1 (0)))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe345
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe346
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe347
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe348
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe349
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe350
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe351
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe352
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1 (0)))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe353
  (((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (R x 0)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe354
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe355
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0)))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe356
  (((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1 (0)))
   ((W z 2)
    (F sync)
    (R x 0)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe357
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (R z 1 (0)))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe358
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R x 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe359
  (((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R x 0)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe360
  (((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe361
  (((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe362
  (((R z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe363
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe364
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe365
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe366
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe367
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe368
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe369
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe370
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe371
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe372
  (((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe373
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe374
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe375
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe376
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe377
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe378
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe379
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe380
  (((R y 2)
    (W x 1 (0)))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe381
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe382
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe383
  (((R y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe384
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe385
  (((R y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe386
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe387
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe388
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe389
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe390
  (((R z 2)
    (W x 1 (0)))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe391
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe392
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe393
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe394
  (((R z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe395
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe396
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe397
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe398
  (((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe399
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe400
  (((R z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe401
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe402
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe403
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe404
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe405
  (((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe406
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe407
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe408
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe409
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe410
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe411
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe412
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe413
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe414
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe415
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe416
  (((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe417
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe418
  (((R z 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe419
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe420
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe421
  (((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe422
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe423
  (((R z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe424
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe425
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe426
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe427
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe428
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe429
  (((W z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R z 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe430
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe431
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe432
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe433
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe434
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe435
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe436
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe437
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe438
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe439
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe440
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe441
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe442
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe443
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe444
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe445
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe446
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe447
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe448
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe449
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe450
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe451
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe452
  (((R y 2)
    (F lwsync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe453
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe454
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe455
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe456
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe457
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe458
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe459
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe460
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe461
  (((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe462
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe463
  (((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe464
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe465
  (((R z 1)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe466
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe467
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe468
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe469
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe470
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe471
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe472
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe473
  (((R x 1)
    (F lwsync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe474
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe475
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe476
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe477
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe478
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe479
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F lwsync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe480
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe481
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe482
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe483
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0))
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe484
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe485
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe486
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe487
  (((R x 1)
    (F sync)
    (R x 1))
   ((W x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe488
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe489
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe490
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe491
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe492
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe493
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe494
  (((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe495
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe496
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe497
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe498
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F sync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe499
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F sync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe500
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)
    (F lwsync)
    (W x 1)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe501
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R y 1))
   ((W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe502
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R z 1))
   ((W z 2)
    (F lwsync)
    (W x 1)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe503
  (((R y 1)
    (F sync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe504
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe505
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe506
  (((R y 2)
    (R x 0 (0))
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe507
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe508
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe509
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe510
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R z 0 (0))
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe511
  (((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe512
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe513
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (R y 1 (0))
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe514
  (((R y 2)
    (W x 1 (0)))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe515
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe516
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe517
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe518
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W z 1 (0)))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe519
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe520
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe521
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (W y 2 (0)))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe522
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe523
  (((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe524
  (((R z 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe525
  (((R y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe526
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe527
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe528
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe529
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe530
  (((R y 2)
    (F sync)
    (R x 0))
   ((W x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe531
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe532
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe533
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F lwsync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe534
  (((R y 2)
    (R x 0 (0))
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe535
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe536
  (((R y 2)
    (W x 1 (0)))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe537
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe538
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe539
  (((R y 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe540
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe541
  (((R y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe542
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe543
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe544
  (((R y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe545
  (((R z 2)
    (R x 0 (0))
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe546
  (((R x 1)
    (R y 0 (0))
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe547
  (((R x 1)
    (R x 1 (0))
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe548
  (((R z 2)
    (W x 1 (0)))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe549
  (((R x 1)
    (W y 1 (0)))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe550
  (((R x 1)
    (W x 2 (0)))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe551
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe552
  (((R z 2)
    (F lwsync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe553
  (((R x 1)
    (F lwsync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F sync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe554
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)
    (F lwsync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe555
  (((R x 1)
    (F lwsync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F sync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe556
  (((R y 1)
    (F sync)
    (W y 2))
   ((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (R y 0))
   ((W y 1)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe557
  (((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W x 1)))
  #:post ((x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe558
  (((R z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe559
  (((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (R a 0))
   ((W a 1)
    (F lwsync)
    (W x 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe560
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (R z 0))
   ((W z 1)
    (F lwsync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe561
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W x 2))
   ((R x 2)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2) (x 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe562
  (((R y 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W y 2)))
  #:post ((y 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe563
  (((R z 2)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W z 2)))
  #:post ((z 2))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe564
  (((R y 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe565
  (((R z 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1)))
  #:allowed vacuous)

(define-litmus-test test/ppc/safe566
  (((R a 1)
    (F sync)
    (W x 1))
   ((R x 1)
    (F sync)
    (W y 1))
   ((R y 1)
    (F sync)
    (W z 1))
   ((R z 1)
    (F sync)
    (W a 1)))
  #:allowed vacuous)

(define all-ppc-tests
  (list test/ppc/aclwdrr000
        test/ppc/aclwdrr001
        test/ppc/aclwdrr002
        test/ppc/aclwdrr003
        test/ppc/aclwdrr004
        test/ppc/aclwdrr005
        test/ppc/aclwdrr006
        test/ppc/aclwdrr007
        test/ppc/aclwdrr008
        test/ppc/aclwdrr009
        test/ppc/aclwdrr010
        test/ppc/aclwdrr011
        test/ppc/aclwdrr012
        test/ppc/aclwdrr013
        test/ppc/aclwdrr014
        test/ppc/aclwdrr015
        test/ppc/aclwdrr016
        test/ppc/aclwdrr017
        test/ppc/aclwdrr018
        test/ppc/aclwdrr019
        test/ppc/aclwdrr020
        test/ppc/aclwdrr021
        test/ppc/aclwdrr022
        test/ppc/aclwdrr023
        test/ppc/aclwdrr024
        test/ppc/aclwdrr025
        test/ppc/aclwdrr026
        test/ppc/aclwdrr027
        test/ppc/aclwdrr028
        test/ppc/aclwdrr029
        test/ppc/aclwdrr030
        test/ppc/aclwdrr031
        test/ppc/aclwdrr032
        test/ppc/aclwdrr033
        test/ppc/aclwdrr034
        test/ppc/aclwdrr035
        test/ppc/aclwdrr036
        test/ppc/aclwdrr037
        test/ppc/aclwdrr038
        test/ppc/aclwdrr039
        test/ppc/aclwdrr040
        test/ppc/aclwdrr041
        test/ppc/aclwdrr042
        test/ppc/aclwsrr000
        test/ppc/aclwsrr001
        test/ppc/aclwsrr002
        test/ppc/aclwsrr003
        test/ppc/aclwsrr004
        test/ppc/aclwsrr005
        test/ppc/aclwsrr006
        test/ppc/aclwsrr007
        test/ppc/bclwdww000
        test/ppc/bclwdww001
        test/ppc/bclwdww002
        test/ppc/bclwdww003
        test/ppc/bclwdww004
        test/ppc/bclwdww005
        test/ppc/bclwdww006
        test/ppc/bclwdww007
        test/ppc/bclwdww008
        test/ppc/bclwdww009
        test/ppc/bclwdww010
        test/ppc/bclwdww011
        test/ppc/bclwdww012
        test/ppc/bclwdww013
        test/ppc/bclwdww014
        test/ppc/bclwdww015
        test/ppc/bclwdww016
        test/ppc/bclwdww017
        test/ppc/bclwdww018
        test/ppc/bclwdww019
        test/ppc/bclwdww020
        test/ppc/bclwdww021
        test/ppc/bclwdww022
        test/ppc/bclwdww023
        test/ppc/bclwdww024
        test/ppc/bclwdww025
        test/ppc/bclwdww026
        test/ppc/bclwdww027
        test/ppc/bclwdww028
        test/ppc/bclwdww029
        test/ppc/bclwdww030
        test/ppc/bclwsww000
        test/ppc/lwdwr020
        test/ppc/lwswr000
        test/ppc/lwswr001
        test/ppc/lwswr002
        test/ppc/lwswr003
        test/ppc/podrr000
        test/ppc/podrr001
        test/ppc/podrr002
        test/ppc/podrr003
        test/ppc/podrr004
        test/ppc/podrr005
        test/ppc/podrr006
        test/ppc/podrr007
        test/ppc/podrr008
        test/ppc/podrr009
        test/ppc/podrr010
        test/ppc/podrr011
        test/ppc/podrw000
        test/ppc/podrw001
        test/ppc/podrw002
        test/ppc/podrw003
        test/ppc/podrw004
        test/ppc/podrwposwr000
        test/ppc/podrwposwr001
        test/ppc/podrwposwr002
        test/ppc/podrwposwr003
        test/ppc/podrwposwr004
        test/ppc/podrwposwr005
        test/ppc/podrwposwr006
        test/ppc/podrwposwr007
        test/ppc/podrwposwr008
        test/ppc/podrwposwr009
        test/ppc/podrwposwr010
        test/ppc/podrwposwr011
        test/ppc/podrwposwr012
        test/ppc/podrwposwr013
        test/ppc/podrwposwr014
        test/ppc/podrwposwr015
        test/ppc/podrwposwr016
        test/ppc/podrwposwr017
        test/ppc/podrwposwr018
        test/ppc/podrwposwr019
        test/ppc/podrwposwr020
        test/ppc/podrwposwr021
        test/ppc/podrwposwr022
        test/ppc/podrwposwr023
        test/ppc/podrwposwr024
        test/ppc/podrwposwr025
        test/ppc/podrwposwr026
        test/ppc/podrwposwr027
        test/ppc/podrwposwr028
        test/ppc/podrwposwr029
        test/ppc/podrwposwr030
        test/ppc/podrwposwr031
        test/ppc/podrwposwr032
        test/ppc/podrwposwr033
        test/ppc/podrwposwr034
        test/ppc/podrwposwr035
        test/ppc/podrwposwr036
        test/ppc/podrwposwr037
        test/ppc/podrwposwr038
        test/ppc/podrwposwr039
        test/ppc/podrwposwr040
        test/ppc/podrwposwr041
        test/ppc/podrwposwr042
        test/ppc/podrwposwr043
        test/ppc/podrwposwr044
        test/ppc/podrwposwr045
        test/ppc/podrwposwr046
        test/ppc/podrwposwr047
        test/ppc/podrwposwr048
        test/ppc/podrwposwr049
        test/ppc/podrwposwr050
        test/ppc/podrwposwr051
        test/ppc/podrwposwr052
        test/ppc/podrwposwr053
        test/ppc/podrwposwr054
        test/ppc/podrwposwr055
        test/ppc/podrwposwr056
        test/ppc/podrwposwr057
        test/ppc/podrwposwr058
        test/ppc/podrwposwr059
        test/ppc/podrwposwr060
        test/ppc/podrwposwr061
        test/ppc/podrwposwr062
        test/ppc/podrwposwr063
        test/ppc/podrwposwr064
        test/ppc/podrwposwr065
        test/ppc/podrwposwr066
        test/ppc/podrwposwr067
        test/ppc/podrwposwr068
        test/ppc/podrwposwr069
        test/ppc/podwr000
        test/ppc/podwr001
        test/ppc/podww000
        test/ppc/podww001
        test/ppc/posrr000
        test/ppc/posrr001
        test/ppc/posrr002
        test/ppc/posrr004
        test/ppc/posrr006
        test/ppc/posrr007
        test/ppc/posrr008
        test/ppc/posrr009
        test/ppc/posrr010
        test/ppc/posrr011
        test/ppc/posrr012
        test/ppc/posrr013
        test/ppc/rfe000
        test/ppc/rfe001
        test/ppc/rfe002
        test/ppc/rfe003
        test/ppc/rfe004
        test/ppc/rfe005
        test/ppc/rfe006
        test/ppc/rfi000
        test/ppc/rfi001
        test/ppc/rfi002
        test/ppc/safe000
        test/ppc/safe001
        test/ppc/safe002
        test/ppc/safe003
        test/ppc/safe004
        test/ppc/safe005
        test/ppc/safe006
        test/ppc/safe007
        test/ppc/safe008
        test/ppc/safe009
        test/ppc/safe010
        test/ppc/safe011
        test/ppc/safe012
        test/ppc/safe013
        test/ppc/safe014
        test/ppc/safe015
        test/ppc/safe016
        test/ppc/safe017
        test/ppc/safe018
        test/ppc/safe019
        test/ppc/safe020
        test/ppc/safe021
        test/ppc/safe022
        test/ppc/safe023
        test/ppc/safe024
        test/ppc/safe025
        test/ppc/safe026
        test/ppc/safe027
        test/ppc/safe028
        test/ppc/safe029
        test/ppc/safe030
        test/ppc/safe031
        test/ppc/safe032
        test/ppc/safe033
        test/ppc/safe034
        test/ppc/safe035
        test/ppc/safe036
        test/ppc/safe037
        test/ppc/safe038
        test/ppc/safe039
        test/ppc/safe040
        test/ppc/safe041
        test/ppc/safe042
        test/ppc/safe043
        test/ppc/safe044
        test/ppc/safe045
        test/ppc/safe046
        test/ppc/safe047
        test/ppc/safe048
        test/ppc/safe049
        test/ppc/safe050
        test/ppc/safe051
        test/ppc/safe052
        test/ppc/safe053
        test/ppc/safe054
        test/ppc/safe055
        test/ppc/safe056
        test/ppc/safe057
        test/ppc/safe058
        test/ppc/safe059
        test/ppc/safe060
        test/ppc/safe061
        test/ppc/safe062
        test/ppc/safe063
        test/ppc/safe064
        test/ppc/safe065
        test/ppc/safe066
        test/ppc/safe067
        test/ppc/safe068
        test/ppc/safe069
        test/ppc/safe070
        test/ppc/safe071
        test/ppc/safe072
        test/ppc/safe073
        test/ppc/safe074
        test/ppc/safe075
        test/ppc/safe076
        test/ppc/safe077
        test/ppc/safe078
        test/ppc/safe079
        test/ppc/safe080
        test/ppc/safe081
        test/ppc/safe082
        test/ppc/safe083
        test/ppc/safe084
        test/ppc/safe085
        test/ppc/safe086
        test/ppc/safe087
        test/ppc/safe088
        test/ppc/safe089
        test/ppc/safe090
        test/ppc/safe091
        test/ppc/safe092
        test/ppc/safe093
        test/ppc/safe094
        test/ppc/safe095
        test/ppc/safe096
        test/ppc/safe097
        test/ppc/safe098
        test/ppc/safe099
        test/ppc/safe100
        test/ppc/safe101
        test/ppc/safe102
        test/ppc/safe103
        test/ppc/safe104
        test/ppc/safe105
        test/ppc/safe106
        test/ppc/safe107
        test/ppc/safe108
        test/ppc/safe109
        test/ppc/safe110
        test/ppc/safe111
        test/ppc/safe112
        test/ppc/safe113
        test/ppc/safe114
        test/ppc/safe115
        test/ppc/safe116
        test/ppc/safe117
        test/ppc/safe118
        test/ppc/safe119
        test/ppc/safe120
        test/ppc/safe121
        test/ppc/safe122
        test/ppc/safe123
        test/ppc/safe124
        test/ppc/safe125
        test/ppc/safe126
        test/ppc/safe127
        test/ppc/safe128
        test/ppc/safe129
        test/ppc/safe130
        test/ppc/safe131
        test/ppc/safe132
        test/ppc/safe133
        test/ppc/safe134
        test/ppc/safe135
        test/ppc/safe136
        test/ppc/safe137
        test/ppc/safe138
        test/ppc/safe139
        test/ppc/safe140
        test/ppc/safe141
        test/ppc/safe142
        test/ppc/safe143
        test/ppc/safe144
        test/ppc/safe145
        test/ppc/safe146
        test/ppc/safe147
        test/ppc/safe148
        test/ppc/safe149
        test/ppc/safe150
        test/ppc/safe151
        test/ppc/safe152
        test/ppc/safe153
        test/ppc/safe154
        test/ppc/safe155
        test/ppc/safe156
        test/ppc/safe157
        test/ppc/safe158
        test/ppc/safe159
        test/ppc/safe160
        test/ppc/safe161
        test/ppc/safe162
        test/ppc/safe163
        test/ppc/safe164
        test/ppc/safe165
        test/ppc/safe166
        test/ppc/safe167
        test/ppc/safe168
        test/ppc/safe169
        test/ppc/safe170
        test/ppc/safe171
        test/ppc/safe172
        test/ppc/safe173
        test/ppc/safe174
        test/ppc/safe175
        test/ppc/safe176
        test/ppc/safe177
        test/ppc/safe178
        test/ppc/safe179
        test/ppc/safe180
        test/ppc/safe181
        test/ppc/safe182
        test/ppc/safe183
        test/ppc/safe184
        test/ppc/safe185
        test/ppc/safe186
        test/ppc/safe187
        test/ppc/safe188
        test/ppc/safe189
        test/ppc/safe190
        test/ppc/safe191
        test/ppc/safe192
        test/ppc/safe193
        test/ppc/safe194
        test/ppc/safe195
        test/ppc/safe196
        test/ppc/safe197
        test/ppc/safe198
        test/ppc/safe199
        test/ppc/safe200
        test/ppc/safe201
        test/ppc/safe202
        test/ppc/safe203
        test/ppc/safe204
        test/ppc/safe205
        test/ppc/safe206
        test/ppc/safe207
        test/ppc/safe208
        test/ppc/safe209
        test/ppc/safe210
        test/ppc/safe211
        test/ppc/safe212
        test/ppc/safe213
        test/ppc/safe214
        test/ppc/safe215
        test/ppc/safe216
        test/ppc/safe217
        test/ppc/safe218
        test/ppc/safe219
        test/ppc/safe220
        test/ppc/safe221
        test/ppc/safe222
        test/ppc/safe223
        test/ppc/safe224
        test/ppc/safe225
        test/ppc/safe226
        test/ppc/safe227
        test/ppc/safe228
        test/ppc/safe229
        test/ppc/safe230
        test/ppc/safe231
        test/ppc/safe232
        test/ppc/safe233
        test/ppc/safe234
        test/ppc/safe235
        test/ppc/safe236
        test/ppc/safe237
        test/ppc/safe238
        test/ppc/safe239
        test/ppc/safe240
        test/ppc/safe241
        test/ppc/safe242
        test/ppc/safe243
        test/ppc/safe244
        test/ppc/safe245
        test/ppc/safe246
        test/ppc/safe247
        test/ppc/safe248
        test/ppc/safe249
        test/ppc/safe250
        test/ppc/safe251
        test/ppc/safe252
        test/ppc/safe253
        test/ppc/safe254
        test/ppc/safe255
        test/ppc/safe256
        test/ppc/safe257
        test/ppc/safe258
        test/ppc/safe259
        test/ppc/safe260
        test/ppc/safe261
        test/ppc/safe262
        test/ppc/safe263
        test/ppc/safe264
        test/ppc/safe265
        test/ppc/safe266
        test/ppc/safe267
        test/ppc/safe268
        test/ppc/safe269
        test/ppc/safe270
        test/ppc/safe271
        test/ppc/safe272
        test/ppc/safe273
        test/ppc/safe274
        test/ppc/safe275
        test/ppc/safe276
        test/ppc/safe277
        test/ppc/safe278
        test/ppc/safe279
        test/ppc/safe280
        test/ppc/safe281
        test/ppc/safe282
        test/ppc/safe283
        test/ppc/safe284
        test/ppc/safe285
        test/ppc/safe286
        test/ppc/safe287
        test/ppc/safe288
        test/ppc/safe289
        test/ppc/safe290
        test/ppc/safe291
        test/ppc/safe292
        test/ppc/safe293
        test/ppc/safe294
        test/ppc/safe295
        test/ppc/safe296
        test/ppc/safe297
        test/ppc/safe298
        test/ppc/safe299
        test/ppc/safe300
        test/ppc/safe301
        test/ppc/safe302
        test/ppc/safe303
        test/ppc/safe304
        test/ppc/safe305
        test/ppc/safe306
        test/ppc/safe307
        test/ppc/safe308
        test/ppc/safe309
        test/ppc/safe310
        test/ppc/safe311
        test/ppc/safe312
        test/ppc/safe313
        test/ppc/safe314
        test/ppc/safe315
        test/ppc/safe316
        test/ppc/safe317
        test/ppc/safe318
        test/ppc/safe319
        test/ppc/safe320
        test/ppc/safe321
        test/ppc/safe322
        test/ppc/safe323
        test/ppc/safe324
        test/ppc/safe325
        test/ppc/safe326
        test/ppc/safe327
        test/ppc/safe328
        test/ppc/safe329
        test/ppc/safe330
        test/ppc/safe331
        test/ppc/safe332
        test/ppc/safe333
        test/ppc/safe334
        test/ppc/safe335
        test/ppc/safe336
        test/ppc/safe337
        test/ppc/safe338
        test/ppc/safe339
        test/ppc/safe340
        test/ppc/safe341
        test/ppc/safe342
        test/ppc/safe343
        test/ppc/safe344
        test/ppc/safe345
        test/ppc/safe346
        test/ppc/safe347
        test/ppc/safe348
        test/ppc/safe349
        test/ppc/safe350
        test/ppc/safe351
        test/ppc/safe352
        test/ppc/safe353
        test/ppc/safe354
        test/ppc/safe355
        test/ppc/safe356
        test/ppc/safe357
        test/ppc/safe358
        test/ppc/safe359
        test/ppc/safe360
        test/ppc/safe361
        test/ppc/safe362
        test/ppc/safe363
        test/ppc/safe364
        test/ppc/safe365
        test/ppc/safe366
        test/ppc/safe367
        test/ppc/safe368
        test/ppc/safe369
        test/ppc/safe370
        test/ppc/safe371
        test/ppc/safe372
        test/ppc/safe373
        test/ppc/safe374
        test/ppc/safe375
        test/ppc/safe376
        test/ppc/safe377
        test/ppc/safe378
        test/ppc/safe379
        test/ppc/safe380
        test/ppc/safe381
        test/ppc/safe382
        test/ppc/safe383
        test/ppc/safe384
        test/ppc/safe385
        test/ppc/safe386
        test/ppc/safe387
        test/ppc/safe388
        test/ppc/safe389
        test/ppc/safe390
        test/ppc/safe391
        test/ppc/safe392
        test/ppc/safe393
        test/ppc/safe394
        test/ppc/safe395
        test/ppc/safe396
        test/ppc/safe397
        test/ppc/safe398
        test/ppc/safe399
        test/ppc/safe400
        test/ppc/safe401
        test/ppc/safe402
        test/ppc/safe403
        test/ppc/safe404
        test/ppc/safe405
        test/ppc/safe406
        test/ppc/safe407
        test/ppc/safe408
        test/ppc/safe409
        test/ppc/safe410
        test/ppc/safe411
        test/ppc/safe412
        test/ppc/safe413
        test/ppc/safe414
        test/ppc/safe415
        test/ppc/safe416
        test/ppc/safe417
        test/ppc/safe418
        test/ppc/safe419
        test/ppc/safe420
        test/ppc/safe421
        test/ppc/safe422
        test/ppc/safe423
        test/ppc/safe424
        test/ppc/safe425
        test/ppc/safe426
        test/ppc/safe427
        test/ppc/safe428
        test/ppc/safe429
        test/ppc/safe430
        test/ppc/safe431
        test/ppc/safe432
        test/ppc/safe433
        test/ppc/safe434
        test/ppc/safe435
        test/ppc/safe436
        test/ppc/safe437
        test/ppc/safe438
        test/ppc/safe439
        test/ppc/safe440
        test/ppc/safe441
        test/ppc/safe442
        test/ppc/safe443
        test/ppc/safe444
        test/ppc/safe445
        test/ppc/safe446
        test/ppc/safe447
        test/ppc/safe448
        test/ppc/safe449
        test/ppc/safe450
        test/ppc/safe451
        test/ppc/safe452
        test/ppc/safe453
        test/ppc/safe454
        test/ppc/safe455
        test/ppc/safe456
        test/ppc/safe457
        test/ppc/safe458
        test/ppc/safe459
        test/ppc/safe460
        test/ppc/safe461
        test/ppc/safe462
        test/ppc/safe463
        test/ppc/safe464
        test/ppc/safe465
        test/ppc/safe466
        test/ppc/safe467
        test/ppc/safe468
        test/ppc/safe469
        test/ppc/safe470
        test/ppc/safe471
        test/ppc/safe472
        test/ppc/safe473
        test/ppc/safe474
        test/ppc/safe475
        test/ppc/safe476
        test/ppc/safe477
        test/ppc/safe478
        test/ppc/safe479
        test/ppc/safe480
        test/ppc/safe481
        test/ppc/safe482
        test/ppc/safe483
        test/ppc/safe484
        test/ppc/safe485
        test/ppc/safe486
        test/ppc/safe487
        test/ppc/safe488
        test/ppc/safe489
        test/ppc/safe490
        test/ppc/safe491
        test/ppc/safe492
        test/ppc/safe493
        test/ppc/safe494
        test/ppc/safe495
        test/ppc/safe496
        test/ppc/safe497
        test/ppc/safe498
        test/ppc/safe499
        test/ppc/safe500
        test/ppc/safe501
        test/ppc/safe502
        test/ppc/safe503
        test/ppc/safe504
        test/ppc/safe505
        test/ppc/safe506
        test/ppc/safe507
        test/ppc/safe508
        test/ppc/safe509
        test/ppc/safe510
        test/ppc/safe511
        test/ppc/safe512
        test/ppc/safe513
        test/ppc/safe514
        test/ppc/safe515
        test/ppc/safe516
        test/ppc/safe517
        test/ppc/safe518
        test/ppc/safe519
        test/ppc/safe520
        test/ppc/safe521
        test/ppc/safe522
        test/ppc/safe523
        test/ppc/safe524
        test/ppc/safe525
        test/ppc/safe526
        test/ppc/safe527
        test/ppc/safe528
        test/ppc/safe529
        test/ppc/safe530
        test/ppc/safe531
        test/ppc/safe532
        test/ppc/safe533
        test/ppc/safe534
        test/ppc/safe535
        test/ppc/safe536
        test/ppc/safe537
        test/ppc/safe538
        test/ppc/safe539
        test/ppc/safe540
        test/ppc/safe541
        test/ppc/safe542
        test/ppc/safe543
        test/ppc/safe544
        test/ppc/safe545
        test/ppc/safe546
        test/ppc/safe547
        test/ppc/safe548
        test/ppc/safe549
        test/ppc/safe550
        test/ppc/safe551
        test/ppc/safe552
        test/ppc/safe553
        test/ppc/safe554
        test/ppc/safe555
        test/ppc/safe556
        test/ppc/safe557
        test/ppc/safe558
        test/ppc/safe559
        test/ppc/safe560
        test/ppc/safe561
        test/ppc/safe562
        test/ppc/safe563
        test/ppc/safe564
        test/ppc/safe565
        test/ppc/safe566))