/* this file tests the various Reach operators */
fail(
""

+           "threshold(true,false,false,false) = "
+     string threshold(true,false,false,false)
+"\n"
+           "threshold(true,true,false,false,false) = "
+     string threshold(true,true,false,false,false)
+"\n"
+           "threshold[3](true,true,false,false,false) = "
+     string threshold[3](true,true,false,false,false)
+"\n"
+           "threshold[3](true,true,true,true,false,false,false) = "
+     string threshold[3](true,true,true,true,false,false,false)
+"\n"


+           "true ? 1 : 2 = "
+     string (true ? 1 : 2)
+"\n"
+           "false ? {1} : {2} = "
+     string (false ? {1} : {2})
+"\n"
+           "true ? 1 : fail \"Oops!\" = "
+     string (true ? 1 : fail "Oops!")
+"\n"
+           "false ? fail \"Oops!\" : 2 = "
+     string (false ? fail "Oops!" : 2)
+"\n"
+           "false ? true ? fail \"Oops2.1!\" : fail \"Oops2.2!\" : 2 = "
+     string (false ? true ? fail "Oops2.1!" : fail "Oops2.2!" : 2)
+"\n"


+           "forall x in {1,2}, y in {3,4} {x<y} = "
+     string forall x in {1,2}, y in {3,4} {x<y}
+"\n"
+           "forall x in {1,2,3}, y in {3,4} {x<y} = "
+     string forall x in {1,2,3}, y in {3,4} {x<y}
+"\n"
+           "forall x in {1,2,3}, y in {3,4} s.t. x%2=0 {x<y} = "
+     string forall x in {1,2,3}, y in {3,4} s.t. x%2=0 {x<y}
+"\n"
+           "exists x in {1,2}, y in {3,4} {x>=y} = "
+     string exists x in {1,2}, y in {3,4} {x>=y}
+"\n"
+           "exists x in {1,2,3}, y in {3,4} {x>=y} = "
+     string exists x in {1,2,3}, y in {3,4} {x>=y}
+"\n"
+           "exists x in {1,2,3}, y in {3,4} s.t. x%2=0 {x>=y} = "
+     string exists x in {1,2,3}, y in {3,4} s.t. x%2=0 {x>=y}
+"\n"
+           "xorsum x in {1,2}, y in {3,4} {x>=y} = "
+     string xorsum x in {1,2}, y in {3,4} {x>=y}
+"\n"
+           "xorsum x in {1,2,3}, y in {3,4} {x>=y} = "
+     string xorsum x in {1,2,3}, y in {3,4} {x>=y}
+"\n"
+           "xorsum x in {1,2,3}, y in {3,4} s.t. x%2=0 {x>=y} = "
+     string xorsum x in {1,2,3}, y in {3,4} s.t. x%2=0 {x>=y}
+"\n"


+           "threshold x in {1,2,5} {x>=5} = "
+     string threshold x in {1,2,5} {x>=5}
+"\n"
+           "threshold x in {1,2,5,6} {x>=5} = "
+     string threshold x in {1,2,5,6} {x>=5}
+"\n"
+           "threshold x in {1,2,5,6} s.t. x%2=0 {x>=5} = "
+     string threshold x in {1,2,5,6} s.t. x%2=0 {x>=5}
+"\n"
+           "threshold[3] x in {1,2,5,6} {x>=5} = "
+     string threshold[3] x in {1,2,5,6} {x>=5}
+"\n"
+           "threshold[3] x in {1,2,5,6,7} {x>=5} = "
+     string threshold[3] x in {1,2,5,6,7} {x>=5}
+"\n"
+           "threshold[3] x in {1,2,5,6,7} s.t. x%2=1 {x>=5} = "
+     string threshold[3] x in {1,2,5,6,7} s.t. x%2=1 {x>=5}
+"\n"

+           "gather x in {1,2,5} {x*x} = "
+     string gather x in {1,2,5} {x*x}
+"\n"
+           "gather x in {1,2,5,6} {x*x} = "
+     string gather x in {1,2,5,6} {x*x}
+"\n"
+           "gather x in {1,2,5,6} s.t. x%2=0 {x*x} = "
+     string gather x in {1,2,5,6} s.t. x%2=0 {x*x}
+"\n"


+           "let x=5 { x+x*x } = "
+     string let x=5 { x+x*x }
+"\n"
+           "let x={3,4},y={5,6} { {{x},{y},{x,y,y}} } = "
+     string let x={3,4},y={5,6} { {{x},{y},{x,y,y}} }
+"\n"
+           "let x={3,4} { {let x=5 { x*x }}+x } = "
+     string let x={3,4} { {let x=5 { x*x }}+x }
+"\n"

)