SMT: Simplify and generalise checking events

SMT query now expressed as a logical expression over events, so e.g.

let default_query =
  Q_or [Q_and [Q_all Assertion; Q_all Return; Q_not (Q_exist Match)]; Q_exist Overflow]

Checks either an overflow occurred, or the function returned true,
while all assertions held, and no match failures occurred. Currently
there is only the default query but the plan is to make this
user-specifiable in the $property/$counterexample directives.

0 files changed, 0 insertions, 0 deletions