Refinement: No artist attempts to register for
e1 when the size of the array used to store artists
e1 is equal to 2.
Pattern: generic check for assertion violations.
Note: This requires the SEDL code to be modified by inserting appropriate assert statements at the points where the array bound could be violated. See the modified SEDL source code.
(defquery "p08a" "nofair" (omega-star-less (sequence (interval :initial t :constraints '((>= "exception(dispatcher;assert)" 1))))))
Up to Property 8: Size of registration list does not exceed 2
Forward to Property 9: INCA
Back to Property 7: INCA