bad-div0.stp

% Trimmed-down example that triggers failures in many different
% STP versions because it causes STP to think about dividing
% by zero.

y : BV(8);

% Should be equivalent to "t4 : BV(8) = 0h01":
t4 : BV(8) = BVPLUS(8, y, BVUMINUS(y), 0h01);

% Should be invalid. Definitely by y = 0h01, but potentially
% also with y = 0h00, if the semantics of divide-by-zero are
% either "always 1" or "could be anything".
QUERY(BVDIV(16, (0h00 @ t4),(0h00 @ y))[0:0] = 0b0);
COUNTEREXAMPLE;