package FloatingPoint;





// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// This module implements division of floating point numbers that conform     //
// with IEEE 754-2008 standard.                                               //
// The algorithm below deals with the full IEEE standard including denormal   //
// and normal numbers, infinity and NaN values.                               //
// ************************************************************************** //

// parameters of the floating-point format
macro MantWidth = 4;
macro ExpWidth  = 3;
macro ExpMax    = exp(2,ExpWidth)-1;
macro ExpBias   = ExpMax / 2;
macro ExpMin    = +1 - ExpBias;
macro Width     = 1+ExpWidth+MantWidth;

macro MantMinNorm = exp(2,MantWidth-1);  // smallest normalized mantissa
macro MantMax     = exp(2,MantWidth)-1;  // largest mantissa value

// macros for extracting parts of the floating point number
macro Sign(x) = x{-1};
macro Exp(x)  = x{-2:MantWidth};
macro Mant(x) = x{MantWidth-1:0};
macro RmHBit(x) = Mant(x);            // remove hidden bit

// macros for interpretation of the floating point numbers
macro ValSign(s)    = (s?-1.0:1.0);
macro ValNMant(m)   = bv2nat(true@m)  * exp(2.0,-1*MantWidth);
macro ValDMant(m)   = bv2nat(false@m) * exp(2.0,-1*MantWidth);
macro ValMant(e,m)  = (e=={false::ExpWidth} ? ValDMant(m) : ValNMant(m));
macro ValNExp(e)    = +bv2nat(e)-ExpBias;
macro ValDExp(e)    = +1-ExpBias;
macro ValExp(e)     = (e=={false::ExpWidth} ? ValDExp(e) : ValNExp(e));
macro Float2Real(x) = ValSign(Sign(x)) * ValMant(Exp(x),Mant(x)) * exp(2.0,ValExp(Exp(x)));

// special values
macro posZero = false@{false::ExpWidth}@{false::MantWidth};
macro negZero =  true@{false::ExpWidth}@{false::MantWidth};
macro posInf  = false@{ true::ExpWidth}@{false::MantWidth};
macro negInf  =  true@{ true::ExpWidth}@{false::MantWidth};
macro posNaN  = false@{ true::ExpWidth}@{ true::MantWidth};
macro negNaN  =  true@{ true::ExpWidth}@{ true::MantWidth};


// Definition of some operations: declaration as macro
macro isZero(x)      = ( ( Exp(x) == {false::ExpWidth} ) & ( Mant(x) == {false::MantWidth} ) );
macro isNormal(x)    = ( 1 <= bv2nat(Exp(x)) ) & ( bv2nat(Exp(x)) <= (exp(2,ExpWidth)-2) );
macro isSubnormal(x) = ( Exp(x) == {false::ExpWidth} ) & ( Mant(x) != {false::MantWidth} );
macro isFinite(x)    = ( isZero(x) | isSubnormal(x) | isNormal(x) );
macro isInfinite(x)  = ( Exp(x) == {true::ExpWidth} ) & ( Mant(x) == {false::MantWidth} );
macro isNaN(x)       = ( Exp(x) == {true::ExpWidth} ) & ( Mant(x) != {false::MantWidth} );
macro isSignMinus(x) = ( Sign(x) != false );

// Macros that return a float
macro fAbs(x)         = (false@Exp(x)@Mant(x));
macro fCopySign(x,y)  = (Sign(y)@Exp(x)@Mant(x));
macro fNegate(x)      = ((Sign(x) ? false : true)@Exp(x)@Mant(x));


// here comes the main module: it first deals with special cases like NaN, Zero and Infinities
// according to the IEEE standard and then (in the largest part of case construct) handles
// normal and denormal numbers

module FloatDiv(bv{Width} ?x,?y,!z,event !rdy) {
    bv{2*MantWidth+2} q;
    int e;
    bool round,sticky;
    bv{ExpWidth}  z_exp;
    bv{MantWidth} z_mnt;

    int ExpCorr;
    int newExp;

    case // define special cases according to IEEE standard
        ( (isZero(x) & isZero(y)) |
          (isInfinite(x) & isInfinite(y)) ) do {
            z = (Sign(x) xor Sign(y) ? negNaN : posNaN);
            emit(rdy);
            }
        (isNaN(x)) do {
            z = x;
            emit(rdy);
            }
        (isNaN(y)) do {
            z = y;
            emit(rdy);
            }
        (isZero(y)) do {
            z = (Sign(y) ? negInf : posInf);
            emit(rdy);
            }
        (isInfinite(y) | isZero(x)) do {
            z = (Sign(x) xor Sign(y) ? negZero : posZero);
            emit(rdy);
            }
    default {
        // left shift x by (MantWidth+1) bits to get a fixed point
        // division where the result has (MantWidth+1) bits precision.
        // The extra bit ("+1") is required to get the q_bit. Moreover
        // the remainder is used to get the sticky_bit (:=(remainder!=0)).
        // Both bits are required to properly round the result.
        // Some examples to visualize the usage of fixed point precision
        // in this module:
        // 1.00 / 1.00 = 100000 / 100 = 001000 = 001.000
        // 1.00 / 0.10 = 100000 / 010 = 010000 = 010.000
        // 1.00 / 0.01 = 100000 / 001 = 100000 = 100.000
        // 0.01 / 1.00 = 001000 / 100 = 000010 = 000.010
        
        let(nx = isNormal(x) )
        let(ny = isNormal(y) )
        let(mx = bv2nat(nx@Mant(x)@{false::(MantWidth+1)}))
        let(my = bv2nat(ny@Mant(y))) {
            q = nat2bv(mx / my, 2*MantWidth+2);

            // NORMALIZE START {
            // Expected position of most-left '1' in q is -(MantWidth+1) (where MSB has -1)
            // Hence, if q=1xxxx then we have to correct the exponent (in a later step) by
            // adding MantWidth+1.
            // Actual position of '1' in q is (at this position) not known. We find it by
            // shifting q left until the MSB is '1'. For each left-shift, the exponent
            // correction must be decremented by 1.
            // Note: All cases that might result in q=0 are handled above, i.e. we
            // eventually have a '1' in q.
            ExpCorr = MantWidth;
            while( !q{-1} ) {
                next(q) = q{-2:0}@false;
                next(ExpCorr) = ExpCorr - 1;
                pause;
            }
            // q = 1xxxxxx;
            sticky = ((mx % my)!=0) | (q{(MantWidth-1):0}!={false::MantWidth}); // remainder of div
            round = q{MantWidth};
            if( (round & sticky) |
                (round & !sticky & q{MantWidth+1}) ) { // round up
                // special case: overflow
                if( q{-1:(MantWidth+1)} == {true::MantWidth} ) {
                    next(q) = true@{false::(2*MantWidth+1)};
                    next(ExpCorr) = ExpCorr + 1;
                } else {
                    next(q) = nat2bv(bv2nat(q{-1:(MantWidth+1)})+1, MantWidth+1)@{false::(MantWidth+1)};
                }
                pause;
            }
            // } NORMALIZE END
        }

        // compute exponent
        case
            (!isSubnormal(x) & !isSubnormal(y)) do {
                newExp = +bv2nat(Exp(x)) - bv2nat(Exp(y)) + ExpBias + ExpCorr;
            }
            (!isSubnormal(x) & isSubnormal(y)) do {
                newExp = +bv2nat(Exp(x)) - ExpMin + ExpCorr;
            }
            (isSubnormal(x) & !isSubnormal(y)) do {
                newExp = +ExpMin - bv2nat(Exp(y)) + 2*ExpBias + ExpCorr;
            }
            (isSubnormal(x) & isSubnormal(y)) do {
                newExp = +ExpBias + ExpCorr;
            }
        default {
            assert(false);
        }

        // check exponent overflow / underflow
        if( newExp > ExpMax ) {
            // overflow ==> return inf
            z = (Sign(x) xor Sign(y) ? negInf : posInf);
        } else if ( newExp < ExpMin ) {
            // underflow ==> denormalize number by right-shift until newExp
            while( newExp < ExpMin ) {
                next(newExp) = newExp + 1;
                next(q) = false@q{-1:1};
                pause;
            }
            z = (Sign(x) xor Sign(y))@{false::ExpWidth}@(q{-1:(MantWidth+2)});
        } else {
            // default: new exponent is in "normal" range => remove hidden bit
            z = (Sign(x) xor Sign(y))@nat2bv(abs(newExp),ExpWidth)@(q{-2:(MantWidth+1)});
        }

        emit(rdy);
    }
}
// ---------------------------------------------
// Cover first case in code
drivenby { // 0
    x = posZero;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 1
    x = posZero;
    y = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 2
    x = negZero;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 3
    x = negZero;
    y = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 4
    x = posInf;
    y = posInf;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 5
    x = posInf;
    y = negInf;
    immediate abort { await(false); } when (rdy);
    assert(z == negNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 6
    x = negInf;
    y = posInf;
    immediate abort { await(false); } when (rdy);
    assert(z == negNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
drivenby { // 7
    x = negInf;
    y = negInf;
    immediate abort { await(false); } when (rdy);
    assert(z == posNaN);
    assert(Sign(z) == Sign(x) xor Sign(y));
}
// ---------------------------------------------
// Cover second case in code
drivenby { // 8
    x = posNaN;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 9
    x = posNaN;
    y = negNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 10
    x = posNaN;
    y = true@0b010@0b1010;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 11
    x = negNaN;
    y = negNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 12
    x = negNaN;
    y = true@0b010@0b1010;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
// ---------------------------------------------
// Cover third case in code
drivenby { // 13
    x = posZero;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
drivenby { // 14
    x = negZero;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
drivenby { // 15
    x = false@0b011@0b1110;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
drivenby { // 16
    x = true@0b110@0b1011;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
drivenby { // 17
    x = negInf;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
drivenby { // 18
    x = posInf;
    y = posNaN;
    immediate abort { await(false); } when (rdy);
    assert(z == y);
}
// ---------------------------------------------
// Cover fourth case in code
drivenby { // 19
    x = false@0b001@0b0011;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == posInf);
}
drivenby { // 20
    x = false@0b101@0b1011;
    y = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negInf);
}
drivenby { // 21
    x = true@0b011@0b1110;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == posInf);
}
drivenby { // 22
    x = true@0b001@0b0001;
    y = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negInf);
}
drivenby { // 23
    x = false@0b011@0b1110;
    y = posZero;
    immediate abort { await(false); } when (rdy);
    assert(z == posInf);
}
drivenby { // 24
    x = true@0b000@0b1110;
    y = negZero;
    immediate abort { await(false); } when (rdy);
    assert(z == negInf);
}
// ---------------------------------------------
// Cover fifth case in code
drivenby { // 25
    x = posZero;
    y = posInf;
    immediate abort { await(false); } when (rdy);
    assert(z == posZero);
}
drivenby { // 26
    x = negZero;
    y = posInf;
    immediate abort { await(false); } when (rdy);
    assert(z == negZero);
}
drivenby { // 27
    x = posZero;
    y = negInf;
    immediate abort { await(false); } when (rdy);
    assert(z == negZero);
}
drivenby { // 28
    x = negZero;
    y = negInf;
    immediate abort { await(false); } when (rdy);
    assert(z == posZero);
}
// ---------------------------------------------
// Cover default case: actual division

// --------------------
// normalized numbers
drivenby { // 29
    x = false@0b011@0b0000;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == false@0b011@0b0000);
}
drivenby { // 30
    x = false@0b110@0b0000;
    y = false@0b110@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == false@0b011@0b0000);
}
drivenby { // 31
    x = false@0b001@0b0000;
    y = false@0b001@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == false@0b011@0b0000);
}

// --------------------
// denormalized numbers
drivenby { // 32
    x = false@0b000@0b0001;
    y = false@0b000@0b0001;
    immediate abort { await(false); } when (rdy);
    assert(z == false@0b011@0b0000);
}
drivenby { // 33
    x = false@0b000@0b1111;
    y = false@0b000@0b1111;
    immediate abort { await(false); } when (rdy);
    assert(z == false@0b011@0b0000);
}

// --------------------
// x / 1 = x
drivenby { // 34
    x = false@0b000@0b0001;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 35
    x = true@0b000@0b1111;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 36
    x = false@0b001@0b0101;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 37
    x = true@0b010@0b1010;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 38
    x = false@0b011@0b1100;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 39
    x = true@0b101@0b0011;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}
drivenby { // 40
    x = false@0b110@0b1101;
    y = false@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == x);
}

// --------------------
// x / -1 = -x
drivenby { // 41
    x = false@0b000@0b0001;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 42
    x = true@0b000@0b1111;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 43
    x = false@0b001@0b0101;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 44
    x = true@0b010@0b1010;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 45
    x = false@0b011@0b1100;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 46
    x = true@0b101@0b0011;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}
drivenby { // 47
    x = false@0b110@0b1101;
    y = true@0b011@0b0000;
    immediate abort { await(false); } when (rdy);
    assert(z == fNegate(x));
}

// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------








// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------
// ------------------------------------------------------------------------------------------
// auto-generated test cases
drivenby { // case 48
  x = (true@0b100@0b1001);
  y = (true@0b101@0b1111);
  // x / y
  // -3.1250000 / -7.7500000 = 0.4032258093357086181641
  // (-1)^(0) * 2^(1 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1010));
}
drivenby { // case 49
  x = (false@0b000@0b0100);
  y = (true@0b010@0b1011);
  // x / y
  // 0.0625000 / -0.8437500 = -0.0740740746259689331055
  // (-1)^(1) * 2^(-1 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 50
  x = (false@0b100@0b1011);
  y = (false@0b011@0b1101);
  // x / y
  // 3.3750000 / 1.8125000 = 1.8620690107345581054688
  // (-1)^(0) * 2^(3 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1110));
}
drivenby { // case 51
  x = (false@0b010@0b1110);
  y = (true@0b001@0b1111);
  // x / y
  // 0.9375000 / -0.4843750 = -1.9354838132858276367188
  // (-1)^(1) * 2^(3 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 52
  x = (true@0b000@0b0011);
  y = (false@0b101@0b0111);
  // x / y
  // -0.0468750 / 5.7500000 = -0.0081521738320589065552
  // (-1)^(1) * 2^(-4 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0000));
}
drivenby { // case 53
  x = (true@0b100@0b0011);
  y = (false@0b011@0b1101);
  // x / y
  // -2.3750000 / 1.8125000 = -1.3103448152542114257812
  // (-1)^(1) * 2^(3 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0101));
}
drivenby { // case 54
  x = (true@0b101@0b1000);
  y = (true@0b010@0b0100);
  // x / y
  // -6.0000000 / -0.6250000 = 9.6000003814697265625000
  // (-1)^(0) * 2^(6 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0011));
}
drivenby { // case 55
  x = (true@0b000@0b0110);
  y = (false@0b001@0b0100);
  // x / y
  // -0.0937500 / 0.3125000 = -0.3000000119209289550781
  // (-1)^(1) * 2^(1 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0011));
}
drivenby { // case 56
  x = (false@0b011@0b1110);
  y = (false@0b100@0b0001);
  // x / y
  // 1.8750000 / 2.1250000 = 0.8823529481887817382812
  // (-1)^(0) * 2^(2 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 57
  x = (true@0b011@0b1100);
  y = (true@0b010@0b1001);
  // x / y
  // -1.7500000 / -0.7812500 = 2.2400000095367431640625
  // (-1)^(0) * 2^(4 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0010));
}
drivenby { // case 58
  x = (false@0b011@0b1110);
  y = (true@0b010@0b1100);
  // x / y
  // 1.8750000 / -0.8750000 = -2.1428570747375488281250
  // (-1)^(1) * 2^(4 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0001));
}
drivenby { // case 59
  x = (true@0b010@0b1111);
  y = (false@0b000@0b0101);
  // x / y
  // -0.9687500 / 0.0781250 = -12.3999996185302734375000
  // (-1)^(1) * 2^(6 - 3) * 11000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b1001));
}
drivenby { // case 60
  x = (false@0b000@0b1101);
  y = (true@0b010@0b1111);
  // x / y
  // 0.2031250 / -0.9687500 = -0.2096774131059646606445
  // (-1)^(1) * 2^(0 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1101));
}
drivenby { // case 61
  x = (false@0b000@0b0110);
  y = (false@0b001@0b1100);
  // x / y
  // 0.0937500 / 0.4375000 = 0.2142857164144515991211
  // (-1)^(0) * 2^(0 - 3) * 11011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1101));
}
drivenby { // case 62
  x = (false@0b000@0b1111);
  y = (true@0b011@0b1010);
  // x / y
  // 0.2343750 / -1.6250000 = -0.1442307680845260620117
  // (-1)^(1) * 2^(0 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 63
  x = (false@0b100@0b1011);
  y = (true@0b101@0b0110);
  // x / y
  // 3.3750000 / -5.5000000 = -0.6136363744735717773438
  // (-1)^(1) * 2^(2 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0100));
}
drivenby { // case 64
  x = (true@0b000@0b1110);
  y = (false@0b001@0b1000);
  // x / y
  // -0.2187500 / 0.3750000 = -0.5833333134651184082031
  // (-1)^(1) * 2^(2 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0011));
}
drivenby { // case 65
  x = (false@0b001@0b1001);
  y = (true@0b100@0b1011);
  // x / y
  // 0.3906250 / -3.3750000 = -0.1157407388091087341309
  // (-1)^(1) * 2^(-1 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 66
  x = (false@0b011@0b1111);
  y = (true@0b011@0b1011);
  // x / y
  // 1.9375000 / -1.6875000 = -1.1481481790542602539062
  // (-1)^(1) * 2^(3 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0010));
}
drivenby { // case 67
  x = (true@0b101@0b0101);
  y = (true@0b011@0b0000);
  // x / y
  // -5.2500000 / -1.0000000 = 5.2500000000000000000000
  // (-1)^(0) * 2^(5 - 3) * 10101 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0101));
}
drivenby { // case 68
  x = (true@0b011@0b1010);
  y = (true@0b100@0b1011);
  // x / y
  // -1.6250000 / -3.3750000 = 0.4814814925193786621094
  // (-1)^(0) * 2^(1 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1111));
}
drivenby { // case 69
  x = (true@0b010@0b1000);
  y = (true@0b010@0b1101);
  // x / y
  // -0.7500000 / -0.9062500 = 0.8275862336158752441406
  // (-1)^(0) * 2^(2 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1010));
}
drivenby { // case 70
  x = (true@0b101@0b1110);
  y = (false@0b100@0b1011);
  // x / y
  // -7.5000000 / 3.3750000 = -2.2222223281860351562500
  // (-1)^(1) * 2^(4 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0010));
}
drivenby { // case 71
  x = (false@0b011@0b0100);
  y = (true@0b010@0b0101);
  // x / y
  // 1.2500000 / -0.6562500 = -1.9047619104385375976562
  // (-1)^(1) * 2^(3 - 3) * 11110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1110));
}
drivenby { // case 72
  x = (false@0b011@0b1001);
  y = (true@0b101@0b0000);
  // x / y
  // 1.5625000 / -4.0000000 = -0.3906250000000000000000
  // (-1)^(1) * 2^(1 - 3) * 11001 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1001));
}
drivenby { // case 73
  x = (false@0b010@0b0001);
  y = (false@0b001@0b1100);
  // x / y
  // 0.5312500 / 0.4375000 = 1.2142857313156127929688
  // (-1)^(0) * 2^(3 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 74
  x = (false@0b100@0b1100);
  y = (false@0b101@0b0000);
  // x / y
  // 3.5000000 / 4.0000000 = 0.8750000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 75
  x = (true@0b011@0b0011);
  y = (true@0b011@0b0000);
  // x / y
  // -1.1875000 / -1.0000000 = 1.1875000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 76
  x = (false@0b101@0b0101);
  y = (false@0b101@0b1111);
  // x / y
  // 5.2500000 / 7.7500000 = 0.6774193644523620605469
  // (-1)^(0) * 2^(2 - 3) * 10101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0110));
}
drivenby { // case 77
  x = (false@0b001@0b1010);
  y = (true@0b101@0b0101);
  // x / y
  // 0.4062500 / -5.2500000 = -0.0773809552192687988281
  // (-1)^(1) * 2^(-1 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0101));
}
drivenby { // case 78
  x = (true@0b001@0b1010);
  y = (false@0b011@0b0011);
  // x / y
  // -0.4062500 / 1.1875000 = -0.3421052694320678710938
  // (-1)^(1) * 2^(1 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0110));
}
drivenby { // case 79
  x = (false@0b011@0b1000);
  y = (false@0b001@0b0011);
  // x / y
  // 1.5000000 / 0.2968750 = 5.0526313781738281250000
  // (-1)^(0) * 2^(5 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0100));
}
drivenby { // case 80
  x = (true@0b010@0b1110);
  y = (false@0b100@0b0010);
  // x / y
  // -0.9375000 / 2.2500000 = -0.4166666567325592041016
  // (-1)^(1) * 2^(1 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1011));
}
drivenby { // case 81
  x = (false@0b000@0b1100);
  y = (true@0b101@0b0100);
  // x / y
  // 0.1875000 / -5.0000000 = -0.0375000014901161193848
  // (-1)^(1) * 2^(-2 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 82
  x = (false@0b011@0b1110);
  y = (true@0b010@0b1011);
  // x / y
  // 1.8750000 / -0.8437500 = -2.2222223281860351562500
  // (-1)^(1) * 2^(4 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0010));
}
drivenby { // case 83
  x = (false@0b101@0b1100);
  y = (false@0b101@0b1011);
  // x / y
  // 7.0000000 / 6.7500000 = 1.0370370149612426757812
  // (-1)^(0) * 2^(3 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0001));
}
drivenby { // case 84
  x = (true@0b011@0b1011);
  y = (false@0b010@0b0011);
  // x / y
  // -1.6875000 / 0.5937500 = -2.8421051502227783203125
  // (-1)^(1) * 2^(4 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0111));
}
drivenby { // case 85
  x = (false@0b000@0b1001);
  y = (true@0b100@0b0000);
  // x / y
  // 0.1406250 / -2.0000000 = -0.0703125000000000000000
  // (-1)^(1) * 2^(-1 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 86
  x = (false@0b100@0b1111);
  y = (false@0b011@0b1001);
  // x / y
  // 3.8750000 / 1.5625000 = 2.4800000190734863281250
  // (-1)^(0) * 2^(4 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0100));
}
drivenby { // case 87
  x = (true@0b000@0b0111);
  y = (true@0b000@0b1000);
  // x / y
  // -0.1093750 / -0.1250000 = 0.8750000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 88
  x = (false@0b000@0b0101);
  y = (true@0b010@0b1000);
  // x / y
  // 0.0781250 / -0.7500000 = -0.1041666641831398010254
  // (-1)^(1) * 2^(-1 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 89
  x = (false@0b010@0b1100);
  y = (true@0b000@0b1100);
  // x / y
  // 0.8750000 / -0.1875000 = -4.6666665077209472656250
  // (-1)^(1) * 2^(5 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0011));
}
drivenby { // case 90
  x = (false@0b000@0b0110);
  y = (true@0b011@0b1110);
  // x / y
  // 0.0937500 / -1.8750000 = -0.0500000007450580596924
  // (-1)^(1) * 2^(-2 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0011));
}
drivenby { // case 91
  x = (false@0b101@0b1101);
  y = (true@0b011@0b0010);
  // x / y
  // 7.2500000 / -1.1250000 = -6.4444446563720703125000
  // (-1)^(1) * 2^(5 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1010));
}
drivenby { // case 92
  x = (true@0b010@0b0100);
  y = (true@0b001@0b1101);
  // x / y
  // -0.6250000 / -0.4531250 = 1.3793103694915771484375
  // (-1)^(0) * 2^(3 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0110));
}
drivenby { // case 93
  x = (true@0b100@0b1111);
  y = (true@0b001@0b0100);
  // x / y
  // -3.8750000 / -0.3125000 = 12.3999996185302734375000
  // (-1)^(0) * 2^(6 - 3) * 11000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b1001));
}
drivenby { // case 94
  x = (false@0b001@0b1110);
  y = (false@0b010@0b1100);
  // x / y
  // 0.4687500 / 0.8750000 = 0.5357142686843872070312
  // (-1)^(0) * 2^(2 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0001));
}
drivenby { // case 95
  x = (true@0b000@0b1101);
  y = (false@0b101@0b0100);
  // x / y
  // -0.2031250 / 5.0000000 = -0.0406249985098838806152
  // (-1)^(1) * 2^(-2 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 96
  x = (false@0b100@0b1011);
  y = (true@0b010@0b1010);
  // x / y
  // 3.3750000 / -0.8125000 = -4.1538462638854980468750
  // (-1)^(1) * 2^(5 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0001));
}
drivenby { // case 97
  x = (true@0b001@0b0011);
  y = (true@0b011@0b0000);
  // x / y
  // -0.2968750 / -1.0000000 = 0.2968750000000000000000
  // (-1)^(0) * 2^(1 - 3) * 10011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0011));
}
drivenby { // case 98
  x = (true@0b001@0b0100);
  y = (true@0b101@0b0100);
  // x / y
  // -0.3125000 / -5.0000000 = 0.0625000000000000000000
  // (-1)^(0) * 2^(-1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0100));
}
drivenby { // case 99
  x = (true@0b010@0b0000);
  y = (false@0b000@0b0100);
  // x / y
  // -0.5000000 / 0.0625000 = -8.0000000000000000000000
  // (-1)^(1) * 2^(6 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b0000));
}
drivenby { // case 100
  x = (false@0b000@0b1100);
  y = (false@0b001@0b1001);
  // x / y
  // 0.1875000 / 0.3906250 = 0.4799999892711639404297
  // (-1)^(0) * 2^(1 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1111));
}
drivenby { // case 101
  x = (false@0b001@0b0000);
  y = (false@0b010@0b1001);
  // x / y
  // 0.2500000 / 0.7812500 = 0.3199999928474426269531
  // (-1)^(0) * 2^(1 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0100));
}
drivenby { // case 102
  x = (false@0b010@0b1100);
  y = (false@0b101@0b0101);
  // x / y
  // 0.8750000 / 5.2500000 = 0.1666666716337203979492
  // (-1)^(0) * 2^(0 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1010));
}
drivenby { // case 103
  x = (true@0b100@0b0100);
  y = (true@0b010@0b0100);
  // x / y
  // -2.5000000 / -0.6250000 = 4.0000000000000000000000
  // (-1)^(0) * 2^(5 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0000));
}
drivenby { // case 104
  x = (false@0b100@0b1011);
  y = (false@0b001@0b0101);
  // x / y
  // 3.3750000 / 0.3281250 = 10.2857141494750976562500
  // (-1)^(0) * 2^(6 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0101));
}
drivenby { // case 105
  x = (true@0b001@0b1000);
  y = (true@0b001@0b0010);
  // x / y
  // -0.3750000 / -0.2812500 = 1.3333333730697631835938
  // (-1)^(0) * 2^(3 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0101));
}
drivenby { // case 106
  x = (false@0b011@0b0000);
  y = (false@0b100@0b0010);
  // x / y
  // 1.0000000 / 2.2500000 = 0.4444444477558135986328
  // (-1)^(0) * 2^(1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1100));
}
drivenby { // case 107
  x = (false@0b001@0b1010);
  y = (false@0b000@0b1010);
  // x / y
  // 0.4062500 / 0.1562500 = 2.5999999046325683593750
  // (-1)^(0) * 2^(4 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 108
  x = (false@0b000@0b0011);
  y = (false@0b000@0b1100);
  // x / y
  // 0.0468750 / 0.1875000 = 0.2500000000000000000000
  // (-1)^(0) * 2^(1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0000));
}
drivenby { // case 109
  x = (true@0b010@0b0111);
  y = (true@0b001@0b0000);
  // x / y
  // -0.7187500 / -0.2500000 = 2.8750000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 10111 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0111));
}
drivenby { // case 110
  x = (false@0b000@0b1111);
  y = (false@0b010@0b1001);
  // x / y
  // 0.2343750 / 0.7812500 = 0.3000000119209289550781
  // (-1)^(0) * 2^(1 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0011));
}
drivenby { // case 111
  x = (false@0b000@0b1110);
  y = (true@0b101@0b1110);
  // x / y
  // 0.2187500 / -7.5000000 = -0.0291666667908430099487
  // (-1)^(1) * 2^(-3 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0001));
}
drivenby { // case 112
  x = (true@0b001@0b0011);
  y = (true@0b101@0b1100);
  // x / y
  // -0.2968750 / -7.0000000 = 0.0424107126891613006592
  // (-1)^(0) * 2^(-2 - 3) * 10101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 113
  x = (false@0b011@0b0000);
  y = (false@0b001@0b0100);
  // x / y
  // 1.0000000 / 0.3125000 = 3.2000000476837158203125
  // (-1)^(0) * 2^(4 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1010));
}
drivenby { // case 114
  x = (true@0b011@0b1100);
  y = (false@0b010@0b0001);
  // x / y
  // -1.7500000 / 0.5312500 = -3.2941176891326904296875
  // (-1)^(1) * 2^(4 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1010));
}
drivenby { // case 115
  x = (false@0b010@0b1100);
  y = (true@0b010@0b1100);
  // x / y
  // 0.8750000 / -0.8750000 = -1.0000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0000));
}
drivenby { // case 116
  x = (false@0b010@0b1010);
  y = (true@0b001@0b0011);
  // x / y
  // 0.8125000 / -0.2968750 = -2.7368421554565429687500
  // (-1)^(1) * 2^(4 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0110));
}
drivenby { // case 117
  x = (true@0b010@0b1100);
  y = (true@0b010@0b1001);
  // x / y
  // -0.8750000 / -0.7812500 = 1.1200000047683715820312
  // (-1)^(0) * 2^(3 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0010));
}
drivenby { // case 118
  x = (true@0b000@0b1111);
  y = (true@0b101@0b0110);
  // x / y
  // -0.2343750 / -5.5000000 = 0.0426136367022991180420
  // (-1)^(0) * 2^(-2 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 119
  x = (true@0b010@0b0111);
  y = (true@0b000@0b0110);
  // x / y
  // -0.7187500 / -0.0937500 = 7.6666665077209472656250
  // (-1)^(0) * 2^(5 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1111));
}
drivenby { // case 120
  x = (true@0b000@0b0110);
  y = (true@0b101@0b1111);
  // x / y
  // -0.0937500 / -7.7500000 = 0.0120967738330364227295
  // (-1)^(0) * 2^(-4 - 3) * 11000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 121
  x = (true@0b100@0b0110);
  y = (true@0b101@0b0001);
  // x / y
  // -2.7500000 / -4.2500000 = 0.6470588445663452148438
  // (-1)^(0) * 2^(2 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 122
  x = (true@0b100@0b0100);
  y = (true@0b101@0b1000);
  // x / y
  // -2.5000000 / -6.0000000 = 0.4166666567325592041016
  // (-1)^(0) * 2^(1 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1011));
}
drivenby { // case 123
  x = (true@0b100@0b0010);
  y = (false@0b011@0b1001);
  // x / y
  // -2.2500000 / 1.5625000 = -1.4400000572204589843750
  // (-1)^(1) * 2^(3 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0111));
}
drivenby { // case 124
  x = (false@0b010@0b0101);
  y = (false@0b000@0b1110);
  // x / y
  // 0.6562500 / 0.2187500 = 3.0000000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1000));
}
drivenby { // case 125
  x = (false@0b101@0b1110);
  y = (false@0b011@0b0110);
  // x / y
  // 7.5000000 / 1.3750000 = 5.4545454978942871093750
  // (-1)^(0) * 2^(5 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0110));
}
drivenby { // case 126
  x = (true@0b100@0b1011);
  y = (false@0b101@0b0001);
  // x / y
  // -3.3750000 / 4.2500000 = -0.7941176295280456542969
  // (-1)^(1) * 2^(2 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1001));
}
drivenby { // case 127
  x = (false@0b010@0b1100);
  y = (true@0b010@0b1001);
  // x / y
  // 0.8750000 / -0.7812500 = -1.1200000047683715820312
  // (-1)^(1) * 2^(3 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0010));
}
drivenby { // case 128
  x = (true@0b010@0b0011);
  y = (true@0b010@0b1001);
  // x / y
  // -0.5937500 / -0.7812500 = 0.7599999904632568359375
  // (-1)^(0) * 2^(2 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1000));
}
drivenby { // case 129
  x = (true@0b100@0b0010);
  y = (false@0b100@0b0100);
  // x / y
  // -2.2500000 / 2.5000000 = -0.8999999761581420898438
  // (-1)^(1) * 2^(2 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1101));
}
drivenby { // case 130
  x = (false@0b011@0b1110);
  y = (false@0b001@0b1101);
  // x / y
  // 1.8750000 / 0.4531250 = 4.1379308700561523437500
  // (-1)^(0) * 2^(5 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0001));
}
drivenby { // case 131
  x = (true@0b001@0b0001);
  y = (false@0b101@0b1111);
  // x / y
  // -0.2656250 / 7.7500000 = -0.0342741943895816802979
  // (-1)^(1) * 2^(-2 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 132
  x = (true@0b010@0b1001);
  y = (true@0b011@0b0011);
  // x / y
  // -0.7812500 / -1.1875000 = 0.6578947305679321289062
  // (-1)^(0) * 2^(2 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 133
  x = (true@0b000@0b1010);
  y = (false@0b011@0b0001);
  // x / y
  // -0.1562500 / 1.0625000 = -0.1470588296651840209961
  // (-1)^(1) * 2^(0 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 134
  x = (false@0b001@0b0010);
  y = (false@0b101@0b1100);
  // x / y
  // 0.2812500 / 7.0000000 = 0.0401785708963871002197
  // (-1)^(0) * 2^(-2 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 135
  x = (false@0b101@0b1101);
  y = (true@0b011@0b0110);
  // x / y
  // 7.2500000 / -1.3750000 = -5.2727274894714355468750
  // (-1)^(1) * 2^(5 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0101));
}
drivenby { // case 136
  x = (false@0b001@0b1001);
  y = (true@0b101@0b1011);
  // x / y
  // 0.3906250 / -6.7500000 = -0.0578703694045543670654
  // (-1)^(1) * 2^(-2 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0011));
}
drivenby { // case 137
  x = (false@0b100@0b0101);
  y = (true@0b011@0b0110);
  // x / y
  // 2.6250000 / -1.3750000 = -1.9090908765792846679688
  // (-1)^(1) * 2^(3 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 138
  x = (false@0b010@0b0100);
  y = (true@0b101@0b1011);
  // x / y
  // 0.6250000 / -6.7500000 = -0.0925925895571708679199
  // (-1)^(1) * 2^(-1 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 139
  x = (true@0b001@0b1001);
  y = (false@0b000@0b0111);
  // x / y
  // -0.3906250 / 0.1093750 = -3.5714285373687744140625
  // (-1)^(1) * 2^(4 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1101));
}
drivenby { // case 140
  x = (false@0b101@0b1001);
  y = (false@0b100@0b1010);
  // x / y
  // 6.2500000 / 3.2500000 = 1.9230768680572509765625
  // (-1)^(0) * 2^(3 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 141
  x = (true@0b011@0b0100);
  y = (false@0b010@0b0100);
  // x / y
  // -1.2500000 / 0.6250000 = -2.0000000000000000000000
  // (-1)^(1) * 2^(4 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0000));
}
drivenby { // case 142
  x = (false@0b011@0b0010);
  y = (false@0b100@0b0011);
  // x / y
  // 1.1250000 / 2.3750000 = 0.4736842215061187744141
  // (-1)^(0) * 2^(1 - 3) * 11110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1110));
}
drivenby { // case 143
  x = (true@0b001@0b0000);
  y = (false@0b000@0b0101);
  // x / y
  // -0.2500000 / 0.0781250 = -3.2000000476837158203125
  // (-1)^(1) * 2^(4 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1010));
}
drivenby { // case 144
  x = (true@0b001@0b1001);
  y = (false@0b011@0b0111);
  // x / y
  // -0.3906250 / 1.4375000 = -0.2717391252517700195312
  // (-1)^(1) * 2^(1 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0001));
}
drivenby { // case 145
  x = (true@0b011@0b1100);
  y = (true@0b101@0b1110);
  // x / y
  // -1.7500000 / -7.5000000 = 0.2333333343267440795898
  // (-1)^(0) * 2^(0 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1111));
}
drivenby { // case 146
  x = (true@0b011@0b1011);
  y = (false@0b001@0b1000);
  // x / y
  // -1.6875000 / 0.3750000 = -4.5000000000000000000000
  // (-1)^(1) * 2^(5 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0010));
}
drivenby { // case 147
  x = (true@0b010@0b0101);
  y = (false@0b010@0b0110);
  // x / y
  // -0.6562500 / 0.6875000 = -0.9545454382896423339844
  // (-1)^(1) * 2^(2 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1111));
}
drivenby { // case 148
  x = (true@0b010@0b0101);
  y = (false@0b100@0b0001);
  // x / y
  // -0.6562500 / 2.1250000 = -0.3088235259056091308594
  // (-1)^(1) * 2^(1 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0100));
}
drivenby { // case 149
  x = (false@0b011@0b1111);
  y = (false@0b010@0b1001);
  // x / y
  // 1.9375000 / 0.7812500 = 2.4800000190734863281250
  // (-1)^(0) * 2^(4 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0100));
}
drivenby { // case 150
  x = (true@0b101@0b1010);
  y = (true@0b010@0b0111);
  // x / y
  // -6.5000000 / -0.7187500 = 9.0434780120849609375000
  // (-1)^(0) * 2^(6 - 3) * 10010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0010));
}
drivenby { // case 151
  x = (false@0b010@0b0110);
  y = (true@0b010@0b1011);
  // x / y
  // 0.6875000 / -0.8437500 = -0.8148148059844970703125
  // (-1)^(1) * 2^(2 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 152
  x = (true@0b011@0b0001);
  y = (true@0b001@0b1000);
  // x / y
  // -1.0625000 / -0.3750000 = 2.8333332538604736328125
  // (-1)^(0) * 2^(4 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0111));
}
drivenby { // case 153
  x = (true@0b001@0b0110);
  y = (false@0b001@0b0100);
  // x / y
  // -0.3437500 / 0.3125000 = -1.1000000238418579101562
  // (-1)^(1) * 2^(3 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0010));
}
drivenby { // case 154
  x = (true@0b011@0b0001);
  y = (true@0b001@0b0001);
  // x / y
  // -1.0625000 / -0.2656250 = 4.0000000000000000000000
  // (-1)^(0) * 2^(5 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0000));
}
drivenby { // case 155
  x = (false@0b001@0b1101);
  y = (false@0b000@0b1011);
  // x / y
  // 0.4531250 / 0.1718750 = 2.6363637447357177734375
  // (-1)^(0) * 2^(4 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 156
  x = (true@0b010@0b0011);
  y = (true@0b001@0b0000);
  // x / y
  // -0.5937500 / -0.2500000 = 2.3750000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 10011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0011));
}
drivenby { // case 157
  x = (true@0b010@0b1011);
  y = (true@0b000@0b0110);
  // x / y
  // -0.8437500 / -0.0937500 = 9.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0010));
}
drivenby { // case 158
  x = (true@0b000@0b1110);
  y = (true@0b000@0b0111);
  // x / y
  // -0.2187500 / -0.1093750 = 2.0000000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 159
  x = (true@0b000@0b0010);
  y = (false@0b001@0b1001);
  // x / y
  // -0.0312500 / 0.3906250 = -0.0799999982118606567383
  // (-1)^(1) * 2^(-1 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0101));
}
drivenby { // case 160
  x = (false@0b010@0b1100);
  y = (true@0b000@0b0100);
  // x / y
  // 0.8750000 / -0.0625000 = -14.0000000000000000000000
  // (-1)^(1) * 2^(6 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b1100));
}
drivenby { // case 161
  x = (true@0b010@0b0110);
  y = (false@0b101@0b1011);
  // x / y
  // -0.6875000 / 6.7500000 = -0.1018518507480621337891
  // (-1)^(1) * 2^(-1 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 162
  x = (false@0b000@0b0110);
  y = (false@0b001@0b0010);
  // x / y
  // 0.0937500 / 0.2812500 = 0.3333333432674407958984
  // (-1)^(0) * 2^(1 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0101));
}
drivenby { // case 163
  x = (true@0b010@0b1010);
  y = (true@0b000@0b1010);
  // x / y
  // -0.8125000 / -0.1562500 = 5.1999998092651367187500
  // (-1)^(0) * 2^(5 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0101));
}
drivenby { // case 164
  x = (false@0b011@0b1010);
  y = (false@0b010@0b0110);
  // x / y
  // 1.6250000 / 0.6875000 = 2.3636362552642822265625
  // (-1)^(0) * 2^(4 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0011));
}
drivenby { // case 165
  x = (true@0b010@0b1110);
  y = (true@0b101@0b1000);
  // x / y
  // -0.9375000 / -6.0000000 = 0.1562500000000000000000
  // (-1)^(0) * 2^(0 - 3) * 10100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1010));
}
drivenby { // case 166
  x = (true@0b010@0b0000);
  y = (false@0b000@0b0011);
  // x / y
  // -0.5000000 / 0.0468750 = -10.6666669845581054687500
  // (-1)^(1) * 2^(6 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b0101));
}
drivenby { // case 167
  x = (true@0b100@0b1101);
  y = (true@0b001@0b1101);
  // x / y
  // -3.6250000 / -0.4531250 = 8.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0000));
}
drivenby { // case 168
  x = (true@0b011@0b1000);
  y = (false@0b001@0b0000);
  // x / y
  // -1.5000000 / 0.2500000 = -6.0000000000000000000000
  // (-1)^(1) * 2^(5 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1000));
}
drivenby { // case 169
  x = (false@0b000@0b0011);
  y = (false@0b011@0b1000);
  // x / y
  // 0.0468750 / 1.5000000 = 0.0312500000000000000000
  // (-1)^(0) * 2^(-2 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 170
  x = (false@0b101@0b1100);
  y = (true@0b011@0b0111);
  // x / y
  // 7.0000000 / -1.4375000 = -4.8695650100708007812500
  // (-1)^(1) * 2^(5 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0011));
}
drivenby { // case 171
  x = (false@0b000@0b1100);
  y = (false@0b001@0b1011);
  // x / y
  // 0.1875000 / 0.4218750 = 0.4444444477558135986328
  // (-1)^(0) * 2^(1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1100));
}
drivenby { // case 172
  x = (false@0b100@0b1101);
  y = (true@0b101@0b1010);
  // x / y
  // 3.6250000 / -6.5000000 = -0.5576922893524169921875
  // (-1)^(1) * 2^(2 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0010));
}
drivenby { // case 173
  x = (false@0b101@0b0010);
  y = (true@0b101@0b0111);
  // x / y
  // 4.5000000 / -5.7500000 = -0.7826086878776550292969
  // (-1)^(1) * 2^(2 - 3) * 11001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1001));
}
drivenby { // case 174
  x = (false@0b001@0b1110);
  y = (false@0b000@0b1101);
  // x / y
  // 0.4687500 / 0.2031250 = 2.3076922893524169921875
  // (-1)^(0) * 2^(4 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0010));
}
drivenby { // case 175
  x = (true@0b011@0b0110);
  y = (true@0b001@0b1011);
  // x / y
  // -1.3750000 / -0.4218750 = 3.2592592239379882812500
  // (-1)^(0) * 2^(4 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1010));
}
drivenby { // case 176
  x = (false@0b101@0b1110);
  y = (true@0b011@0b0111);
  // x / y
  // 7.5000000 / -1.4375000 = -5.2173914909362792968750
  // (-1)^(1) * 2^(5 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0101));
}
drivenby { // case 177
  x = (false@0b011@0b1100);
  y = (false@0b100@0b0111);
  // x / y
  // 1.7500000 / 2.8750000 = 0.6086956262588500976562
  // (-1)^(0) * 2^(2 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0011));
}
drivenby { // case 178
  x = (true@0b100@0b1110);
  y = (true@0b100@0b1111);
  // x / y
  // -3.7500000 / -3.8750000 = 0.9677419066429138183594
  // (-1)^(0) * 2^(2 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1111));
}
drivenby { // case 179
  x = (true@0b010@0b0011);
  y = (true@0b000@0b0100);
  // x / y
  // -0.5937500 / -0.0625000 = 9.5000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0011));
}
drivenby { // case 180
  x = (true@0b100@0b1010);
  y = (true@0b001@0b1011);
  // x / y
  // -3.2500000 / -0.4218750 = 7.7037038803100585937500
  // (-1)^(0) * 2^(5 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1111));
}
drivenby { // case 181
  x = (false@0b010@0b1101);
  y = (false@0b001@0b1100);
  // x / y
  // 0.9062500 / 0.4375000 = 2.0714285373687744140625
  // (-1)^(0) * 2^(4 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0001));
}
drivenby { // case 182
  x = (false@0b011@0b0101);
  y = (false@0b101@0b0010);
  // x / y
  // 1.3125000 / 4.5000000 = 0.2916666567325592041016
  // (-1)^(0) * 2^(1 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0011));
}
drivenby { // case 183
  x = (false@0b011@0b0010);
  y = (false@0b100@0b1100);
  // x / y
  // 1.1250000 / 3.5000000 = 0.3214285671710968017578
  // (-1)^(0) * 2^(1 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0101));
}
drivenby { // case 184
  x = (false@0b011@0b1000);
  y = (true@0b101@0b0010);
  // x / y
  // 1.5000000 / -4.5000000 = -0.3333333432674407958984
  // (-1)^(1) * 2^(1 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0101));
}
drivenby { // case 185
  x = (false@0b000@0b1001);
  y = (true@0b101@0b0000);
  // x / y
  // 0.1406250 / -4.0000000 = -0.0351562500000000000000
  // (-1)^(1) * 2^(-2 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 186
  x = (false@0b011@0b0110);
  y = (true@0b100@0b0001);
  // x / y
  // 1.3750000 / -2.1250000 = -0.6470588445663452148438
  // (-1)^(1) * 2^(2 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0101));
}
drivenby { // case 187
  x = (true@0b100@0b0001);
  y = (true@0b011@0b0110);
  // x / y
  // -2.1250000 / -1.3750000 = 1.5454545021057128906250
  // (-1)^(0) * 2^(3 - 3) * 11000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1001));
}
drivenby { // case 188
  x = (true@0b001@0b1011);
  y = (true@0b010@0b0000);
  // x / y
  // -0.4218750 / -0.5000000 = 0.8437500000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1011));
}
drivenby { // case 189
  x = (true@0b010@0b0000);
  y = (false@0b101@0b0001);
  // x / y
  // -0.5000000 / 4.2500000 = -0.1176470592617988586426
  // (-1)^(1) * 2^(-1 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 190
  x = (false@0b000@0b1111);
  y = (false@0b001@0b0111);
  // x / y
  // 0.2343750 / 0.3593750 = 0.6521739363670349121094
  // (-1)^(0) * 2^(2 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 191
  x = (true@0b101@0b0001);
  y = (false@0b100@0b1001);
  // x / y
  // -4.2500000 / 3.1250000 = -1.3600000143051147460938
  // (-1)^(1) * 2^(3 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0110));
}
drivenby { // case 192
  x = (true@0b001@0b1000);
  y = (false@0b010@0b1011);
  // x / y
  // -0.3750000 / 0.8437500 = -0.4444444477558135986328
  // (-1)^(1) * 2^(1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1100));
}
drivenby { // case 193
  x = (false@0b101@0b0010);
  y = (false@0b010@0b0000);
  // x / y
  // 4.5000000 / 0.5000000 = 9.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0010));
}
drivenby { // case 194
  x = (false@0b001@0b1000);
  y = (true@0b101@0b1011);
  // x / y
  // 0.3750000 / -6.7500000 = -0.0555555559694766998291
  // (-1)^(1) * 2^(-2 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0011));
}
drivenby { // case 195
  x = (false@0b001@0b1110);
  y = (true@0b101@0b0110);
  // x / y
  // 0.4687500 / -5.5000000 = -0.0852272734045982360840
  // (-1)^(1) * 2^(-1 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0101));
}
drivenby { // case 196
  x = (true@0b100@0b0101);
  y = (true@0b101@0b1101);
  // x / y
  // -2.6250000 / -7.2500000 = 0.3620689511299133300781
  // (-1)^(0) * 2^(1 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0111));
}
drivenby { // case 197
  x = (false@0b100@0b1110);
  y = (false@0b101@0b1001);
  // x / y
  // 3.7500000 / 6.2500000 = 0.6000000238418579101562
  // (-1)^(0) * 2^(2 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0011));
}
drivenby { // case 198
  x = (false@0b101@0b0111);
  y = (false@0b011@0b1100);
  // x / y
  // 5.7500000 / 1.7500000 = 3.2857143878936767578125
  // (-1)^(0) * 2^(4 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1010));
}
drivenby { // case 199
  x = (false@0b001@0b1011);
  y = (false@0b101@0b0001);
  // x / y
  // 0.4218750 / 4.2500000 = 0.0992647036910057067871
  // (-1)^(0) * 2^(-1 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0110));
}
drivenby { // case 200
  x = (true@0b100@0b0111);
  y = (false@0b011@0b0000);
  // x / y
  // -2.8750000 / 1.0000000 = -2.8750000000000000000000
  // (-1)^(1) * 2^(4 - 3) * 10111 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0111));
}
drivenby { // case 201
  x = (false@0b101@0b0010);
  y = (false@0b001@0b0111);
  // x / y
  // 4.5000000 / 0.3593750 = 12.5217390060424804687500
  // (-1)^(0) * 2^(6 - 3) * 11001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b1001));
}
drivenby { // case 202
  x = (true@0b001@0b0001);
  y = (true@0b001@0b0000);
  // x / y
  // -0.2656250 / -0.2500000 = 1.0625000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10001 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0001));
}
drivenby { // case 203
  x = (false@0b010@0b1000);
  y = (true@0b011@0b1101);
  // x / y
  // 0.7500000 / -1.8125000 = -0.4137931168079376220703
  // (-1)^(1) * 2^(1 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1010));
}
drivenby { // case 204
  x = (false@0b010@0b1001);
  y = (false@0b010@0b0100);
  // x / y
  // 0.7812500 / 0.6250000 = 1.2500000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 205
  x = (false@0b000@0b1100);
  y = (false@0b101@0b1010);
  // x / y
  // 0.1875000 / 6.5000000 = 0.0288461539894342422485
  // (-1)^(0) * 2^(-3 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0001));
}
drivenby { // case 206
  x = (false@0b010@0b0111);
  y = (true@0b001@0b1111);
  // x / y
  // 0.7187500 / -0.4843750 = -1.4838709831237792968750
  // (-1)^(1) * 2^(3 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 207
  x = (false@0b001@0b1001);
  y = (false@0b101@0b1101);
  // x / y
  // 0.3906250 / 7.2500000 = 0.0538793094456195831299
  // (-1)^(0) * 2^(-2 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 208
  x = (true@0b001@0b1000);
  y = (true@0b100@0b0111);
  // x / y
  // -0.3750000 / -2.8750000 = 0.1304347813129425048828
  // (-1)^(0) * 2^(0 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1000));
}
drivenby { // case 209
  x = (true@0b101@0b0001);
  y = (false@0b011@0b1011);
  // x / y
  // -4.2500000 / 1.6875000 = -2.5185184478759765625000
  // (-1)^(1) * 2^(4 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0100));
}
drivenby { // case 210
  x = (true@0b001@0b0100);
  y = (false@0b100@0b0101);
  // x / y
  // -0.3125000 / 2.6250000 = -0.1190476194024085998535
  // (-1)^(1) * 2^(-1 - 3) * 11110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 211
  x = (true@0b100@0b0011);
  y = (false@0b101@0b1100);
  // x / y
  // -2.3750000 / 7.0000000 = -0.3392857015132904052734
  // (-1)^(1) * 2^(1 - 3) * 10101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0110));
}
drivenby { // case 212
  x = (true@0b011@0b1001);
  y = (false@0b001@0b0010);
  // x / y
  // -1.5625000 / 0.2812500 = -5.5555553436279296875000
  // (-1)^(1) * 2^(5 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0110));
}
drivenby { // case 213
  x = (false@0b010@0b0011);
  y = (false@0b100@0b1000);
  // x / y
  // 0.5937500 / 3.0000000 = 0.1979166716337203979492
  // (-1)^(0) * 2^(0 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1100));
}
drivenby { // case 214
  x = (true@0b011@0b0001);
  y = (false@0b011@0b0110);
  // x / y
  // -1.0625000 / 1.3750000 = -0.7727272510528564453125
  // (-1)^(1) * 2^(2 - 3) * 11000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1001));
}
drivenby { // case 215
  x = (true@0b000@0b0011);
  y = (true@0b011@0b0111);
  // x / y
  // -0.0468750 / -1.4375000 = 0.0326086953282356262207
  // (-1)^(0) * 2^(-2 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 216
  x = (true@0b010@0b0110);
  y = (true@0b100@0b0000);
  // x / y
  // -0.6875000 / -2.0000000 = 0.3437500000000000000000
  // (-1)^(0) * 2^(1 - 3) * 10110 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0110));
}
drivenby { // case 217
  x = (true@0b000@0b1000);
  y = (false@0b011@0b0111);
  // x / y
  // -0.1250000 / 1.4375000 = -0.0869565233588218688965
  // (-1)^(1) * 2^(-1 - 3) * 10110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0101));
}
drivenby { // case 218
  x = (false@0b100@0b0010);
  y = (false@0b001@0b1000);
  // x / y
  // 2.2500000 / 0.3750000 = 6.0000000000000000000000
  // (-1)^(0) * 2^(5 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1000));
}
drivenby { // case 219
  x = (true@0b000@0b1001);
  y = (false@0b010@0b1111);
  // x / y
  // -0.1406250 / 0.9687500 = -0.1451612859964370727539
  // (-1)^(1) * 2^(0 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 220
  x = (true@0b100@0b1100);
  y = (true@0b010@0b1101);
  // x / y
  // -3.5000000 / -0.9062500 = 3.8620688915252685546875
  // (-1)^(0) * 2^(4 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1111));
}
drivenby { // case 221
  x = (true@0b011@0b0110);
  y = (false@0b101@0b1010);
  // x / y
  // -1.3750000 / 6.5000000 = -0.2115384638309478759766
  // (-1)^(1) * 2^(0 - 3) * 11011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1101));
}
drivenby { // case 222
  x = (true@0b001@0b0110);
  y = (false@0b011@0b0011);
  // x / y
  // -0.3437500 / 1.1875000 = -0.2894736826419830322266
  // (-1)^(1) * 2^(1 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0011));
}
drivenby { // case 223
  x = (true@0b101@0b0100);
  y = (true@0b011@0b1011);
  // x / y
  // -5.0000000 / -1.6875000 = 2.9629628658294677734375
  // (-1)^(0) * 2^(4 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1000));
}
drivenby { // case 224
  x = (false@0b000@0b0001);
  y = (false@0b101@0b1000);
  // x / y
  // 0.0156250 / 6.0000000 = 0.0026041667442768812180
  // (-1)^(0) * 2^(-6 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 225
  x = (true@0b100@0b0101);
  y = (false@0b101@0b1111);
  // x / y
  // -2.6250000 / 7.7500000 = -0.3387096822261810302734
  // (-1)^(1) * 2^(1 - 3) * 10101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0110));
}
drivenby { // case 226
  x = (true@0b011@0b1110);
  y = (true@0b101@0b1111);
  // x / y
  // -1.8750000 / -7.7500000 = 0.2419354766607284545898
  // (-1)^(0) * 2^(0 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1111));
}
drivenby { // case 227
  x = (true@0b010@0b1110);
  y = (false@0b100@0b1011);
  // x / y
  // -0.9375000 / 3.3750000 = -0.2777777910232543945312
  // (-1)^(1) * 2^(1 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0010));
}
drivenby { // case 228
  x = (true@0b001@0b1010);
  y = (true@0b011@0b0010);
  // x / y
  // -0.4062500 / -1.1250000 = 0.3611111044883728027344
  // (-1)^(0) * 2^(1 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0111));
}
drivenby { // case 229
  x = (true@0b101@0b0010);
  y = (true@0b101@0b1011);
  // x / y
  // -4.5000000 / -6.7500000 = 0.6666666865348815917969
  // (-1)^(0) * 2^(2 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 230
  x = (true@0b100@0b1010);
  y = (false@0b010@0b1011);
  // x / y
  // -3.2500000 / 0.8437500 = -3.8518519401550292968750
  // (-1)^(1) * 2^(4 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1111));
}
drivenby { // case 231
  x = (true@0b001@0b1010);
  y = (true@0b000@0b1010);
  // x / y
  // -0.4062500 / -0.1562500 = 2.5999999046325683593750
  // (-1)^(0) * 2^(4 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 232
  x = (true@0b100@0b1101);
  y = (true@0b010@0b0011);
  // x / y
  // -3.6250000 / -0.5937500 = 6.1052632331848144531250
  // (-1)^(0) * 2^(5 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1000));
}
drivenby { // case 233
  x = (true@0b100@0b0101);
  y = (false@0b001@0b1010);
  // x / y
  // -2.6250000 / 0.4062500 = -6.4615383148193359375000
  // (-1)^(1) * 2^(5 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1010));
}
drivenby { // case 234
  x = (true@0b010@0b0000);
  y = (true@0b001@0b0101);
  // x / y
  // -0.5000000 / -0.3281250 = 1.5238095521926879882812
  // (-1)^(0) * 2^(3 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1000));
}
drivenby { // case 235
  x = (true@0b100@0b0100);
  y = (true@0b010@0b0101);
  // x / y
  // -2.5000000 / -0.6562500 = 3.8095238208770751953125
  // (-1)^(0) * 2^(4 - 3) * 11110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1110));
}
drivenby { // case 236
  x = (true@0b101@0b0001);
  y = (false@0b010@0b1111);
  // x / y
  // -4.2500000 / 0.9687500 = -4.3870968818664550781250
  // (-1)^(1) * 2^(5 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0010));
}
drivenby { // case 237
  x = (false@0b101@0b0010);
  y = (true@0b011@0b1111);
  // x / y
  // 4.5000000 / -1.9375000 = -2.3225805759429931640625
  // (-1)^(1) * 2^(4 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0011));
}
drivenby { // case 238
  x = (true@0b010@0b0001);
  y = (false@0b010@0b1010);
  // x / y
  // -0.5312500 / 0.8125000 = -0.6538461446762084960938
  // (-1)^(1) * 2^(2 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0101));
}
drivenby { // case 239
  x = (false@0b000@0b1001);
  y = (false@0b001@0b0000);
  // x / y
  // 0.1406250 / 0.2500000 = 0.5625000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0010));
}
drivenby { // case 240
  x = (true@0b010@0b0000);
  y = (false@0b000@0b1001);
  // x / y
  // -0.5000000 / 0.1406250 = -3.5555555820465087890625
  // (-1)^(1) * 2^(4 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1100));
}
drivenby { // case 241
  x = (true@0b101@0b0101);
  y = (false@0b011@0b1000);
  // x / y
  // -5.2500000 / 1.5000000 = -3.5000000000000000000000
  // (-1)^(1) * 2^(4 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1100));
}
drivenby { // case 242
  x = (true@0b011@0b0101);
  y = (true@0b010@0b1000);
  // x / y
  // -1.3125000 / -0.7500000 = 1.7500000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1100));
}
drivenby { // case 243
  x = (true@0b011@0b0011);
  y = (false@0b101@0b0111);
  // x / y
  // -1.1875000 / 5.7500000 = -0.2065217345952987670898
  // (-1)^(1) * 2^(0 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1101));
}
drivenby { // case 244
  x = (true@0b101@0b0001);
  y = (false@0b010@0b1011);
  // x / y
  // -4.2500000 / 0.8437500 = -5.0370368957519531250000
  // (-1)^(1) * 2^(5 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0100));
}
drivenby { // case 245
  x = (false@0b001@0b1111);
  y = (false@0b001@0b1001);
  // x / y
  // 0.4843750 / 0.3906250 = 1.2400000095367431640625
  // (-1)^(0) * 2^(3 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 246
  x = (false@0b011@0b0101);
  y = (false@0b011@0b1010);
  // x / y
  // 1.3125000 / 1.6250000 = 0.8076922893524169921875
  // (-1)^(0) * 2^(2 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1010));
}
drivenby { // case 247
  x = (false@0b100@0b1011);
  y = (true@0b100@0b1111);
  // x / y
  // 3.3750000 / -3.8750000 = -0.8709677457809448242188
  // (-1)^(1) * 2^(2 - 3) * 11011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1100));
}
drivenby { // case 248
  x = (true@0b011@0b1110);
  y = (false@0b101@0b1010);
  // x / y
  // -1.8750000 / 6.5000000 = -0.2884615361690521240234
  // (-1)^(1) * 2^(1 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0010));
}
drivenby { // case 249
  x = (true@0b001@0b1000);
  y = (true@0b100@0b1011);
  // x / y
  // -0.3750000 / -3.3750000 = 0.1111111119389533996582
  // (-1)^(0) * 2^(-1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0111));
}
drivenby { // case 250
  x = (false@0b101@0b1010);
  y = (true@0b101@0b0100);
  // x / y
  // 6.5000000 / -5.0000000 = -1.2999999523162841796875
  // (-1)^(1) * 2^(3 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0101));
}
drivenby { // case 251
  x = (true@0b000@0b1101);
  y = (false@0b000@0b1110);
  // x / y
  // -0.2031250 / 0.2187500 = -0.9285714030265808105469
  // (-1)^(1) * 2^(2 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1110));
}
drivenby { // case 252
  x = (false@0b010@0b1101);
  y = (false@0b000@0b1101);
  // x / y
  // 0.9062500 / 0.2031250 = 4.4615383148193359375000
  // (-1)^(0) * 2^(5 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0010));
}
drivenby { // case 253
  x = (true@0b101@0b0011);
  y = (true@0b101@0b0110);
  // x / y
  // -4.7500000 / -5.5000000 = 0.8636363744735717773438
  // (-1)^(0) * 2^(2 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 254
  x = (false@0b101@0b0110);
  y = (false@0b100@0b0010);
  // x / y
  // 5.5000000 / 2.2500000 = 2.4444444179534912109375
  // (-1)^(0) * 2^(4 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0100));
}
drivenby { // case 255
  x = (true@0b100@0b1101);
  y = (true@0b001@0b1100);
  // x / y
  // -3.6250000 / -0.4375000 = 8.2857141494750976562500
  // (-1)^(0) * 2^(6 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0001));
}
drivenby { // case 256
  x = (false@0b000@0b0100);
  y = (false@0b001@0b0110);
  // x / y
  // 0.0625000 / 0.3437500 = 0.1818181872367858886719
  // (-1)^(0) * 2^(0 - 3) * 10111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1011));
}
drivenby { // case 257
  x = (true@0b101@0b1111);
  y = (false@0b101@0b0101);
  // x / y
  // -7.7500000 / 5.2500000 = -1.4761904478073120117188
  // (-1)^(1) * 2^(3 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 258
  x = (true@0b010@0b0000);
  y = (false@0b010@0b0001);
  // x / y
  // -0.5000000 / 0.5312500 = -0.9411764740943908691406
  // (-1)^(1) * 2^(2 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1110));
}
drivenby { // case 259
  x = (true@0b000@0b0010);
  y = (true@0b010@0b1000);
  // x / y
  // -0.0312500 / -0.7500000 = 0.0416666679084300994873
  // (-1)^(0) * 2^(-2 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 260
  x = (true@0b011@0b0111);
  y = (false@0b101@0b1110);
  // x / y
  // -1.4375000 / 7.5000000 = -0.1916666626930236816406
  // (-1)^(1) * 2^(0 - 3) * 11000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1100));
}
drivenby { // case 261
  x = (false@0b011@0b1011);
  y = (true@0b011@0b0010);
  // x / y
  // 1.6875000 / -1.1250000 = -1.5000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 262
  x = (true@0b100@0b1101);
  y = (false@0b010@0b1001);
  // x / y
  // -3.6250000 / 0.7812500 = -4.6399998664855957031250
  // (-1)^(1) * 2^(5 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0011));
}
drivenby { // case 263
  x = (true@0b011@0b0011);
  y = (true@0b010@0b1011);
  // x / y
  // -1.1875000 / -0.8437500 = 1.4074074029922485351562
  // (-1)^(0) * 2^(3 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0111));
}
drivenby { // case 264
  x = (true@0b011@0b1011);
  y = (true@0b010@0b1011);
  // x / y
  // -1.6875000 / -0.8437500 = 2.0000000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0000));
}
drivenby { // case 265
  x = (false@0b101@0b0111);
  y = (true@0b001@0b1000);
  // x / y
  // 5.7500000 / -0.3750000 = -15.3333330154418945312500
  // (-1)^(1) * 2^(6 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b1111));
}
drivenby { // case 266
  x = (true@0b011@0b0011);
  y = (false@0b010@0b0010);
  // x / y
  // -1.1875000 / 0.5625000 = -2.1111111640930175781250
  // (-1)^(1) * 2^(4 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0001));
}
drivenby { // case 267
  x = (false@0b010@0b0010);
  y = (false@0b010@0b0000);
  // x / y
  // 0.5625000 / 0.5000000 = 1.1250000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0010));
}
drivenby { // case 268
  x = (true@0b000@0b0011);
  y = (false@0b001@0b1011);
  // x / y
  // -0.0468750 / 0.4218750 = -0.1111111119389533996582
  // (-1)^(1) * 2^(-1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 269
  x = (false@0b000@0b0001);
  y = (true@0b000@0b1001);
  // x / y
  // 0.0156250 / -0.1406250 = -0.1111111119389533996582
  // (-1)^(1) * 2^(-1 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 270
  x = (true@0b000@0b1110);
  y = (false@0b001@0b0000);
  // x / y
  // -0.2187500 / 0.2500000 = -0.8750000000000000000000
  // (-1)^(1) * 2^(2 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1100));
}
drivenby { // case 271
  x = (false@0b010@0b1000);
  y = (true@0b101@0b1100);
  // x / y
  // 0.7500000 / -7.0000000 = -0.1071428582072257995605
  // (-1)^(1) * 2^(-1 - 3) * 11011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 272
  x = (true@0b011@0b0100);
  y = (true@0b001@0b1111);
  // x / y
  // -1.2500000 / -0.4843750 = 2.5806450843811035156250
  // (-1)^(0) * 2^(4 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 273
  x = (true@0b100@0b0001);
  y = (false@0b101@0b1010);
  // x / y
  // -2.1250000 / 6.5000000 = -0.3269230723381042480469
  // (-1)^(1) * 2^(1 - 3) * 10100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0101));
}
drivenby { // case 274
  x = (true@0b101@0b0011);
  y = (false@0b011@0b0110);
  // x / y
  // -4.7500000 / 1.3750000 = -3.4545454978942871093750
  // (-1)^(1) * 2^(4 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1100));
}
drivenby { // case 275
  x = (true@0b011@0b0100);
  y = (true@0b100@0b1001);
  // x / y
  // -1.2500000 / -3.1250000 = 0.4000000059604644775391
  // (-1)^(0) * 2^(1 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1010));
}
drivenby { // case 276
  x = (true@0b101@0b0111);
  y = (false@0b100@0b1010);
  // x / y
  // -5.7500000 / 3.2500000 = -1.7692307233810424804688
  // (-1)^(1) * 2^(3 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1100));
}
drivenby { // case 277
  x = (true@0b011@0b1101);
  y = (false@0b010@0b0010);
  // x / y
  // -1.8125000 / 0.5625000 = -3.2222223281860351562500
  // (-1)^(1) * 2^(4 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1010));
}
drivenby { // case 278
  x = (false@0b000@0b0010);
  y = (true@0b000@0b1000);
  // x / y
  // 0.0312500 / -0.1250000 = -0.2500000000000000000000
  // (-1)^(1) * 2^(1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0000));
}
drivenby { // case 279
  x = (false@0b001@0b0011);
  y = (true@0b100@0b0000);
  // x / y
  // 0.2968750 / -2.0000000 = -0.1484375000000000000000
  // (-1)^(1) * 2^(0 - 3) * 10011 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 280
  x = (true@0b011@0b0010);
  y = (false@0b000@0b0101);
  // x / y
  // -1.1250000 / 0.0781250 = -14.3999996185302734375000
  // (-1)^(1) * 2^(6 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b1101));
}
drivenby { // case 281
  x = (true@0b011@0b1100);
  y = (false@0b011@0b1000);
  // x / y
  // -1.7500000 / 1.5000000 = -1.1666666269302368164062
  // (-1)^(1) * 2^(3 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0011));
}
drivenby { // case 282
  x = (true@0b010@0b0000);
  y = (false@0b010@0b1010);
  // x / y
  // -0.5000000 / 0.8125000 = -0.6153846383094787597656
  // (-1)^(1) * 2^(2 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0100));
}
drivenby { // case 283
  x = (false@0b001@0b0010);
  y = (true@0b010@0b1010);
  // x / y
  // 0.2812500 / -0.8125000 = -0.3461538553237915039062
  // (-1)^(1) * 2^(1 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0110));
}
drivenby { // case 284
  x = (false@0b101@0b0110);
  y = (true@0b010@0b0010);
  // x / y
  // 5.5000000 / -0.5625000 = -9.7777776718139648437500
  // (-1)^(1) * 2^(6 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b0100));
}
drivenby { // case 285
  x = (false@0b000@0b1111);
  y = (false@0b100@0b0101);
  // x / y
  // 0.2343750 / 2.6250000 = 0.0892857164144515991211
  // (-1)^(0) * 2^(-1 - 3) * 10110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0101));
}
drivenby { // case 286
  x = (false@0b101@0b0000);
  y = (false@0b100@0b0110);
  // x / y
  // 4.0000000 / 2.7500000 = 1.4545454978942871093750
  // (-1)^(0) * 2^(3 - 3) * 10111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0111));
}
drivenby { // case 287
  x = (true@0b001@0b0100);
  y = (true@0b011@0b1101);
  // x / y
  // -0.3125000 / -1.8125000 = 0.1724137961864471435547
  // (-1)^(0) * 2^(0 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1011));
}
drivenby { // case 288
  x = (true@0b011@0b1010);
  y = (true@0b010@0b1000);
  // x / y
  // -1.6250000 / -0.7500000 = 2.1666667461395263671875
  // (-1)^(0) * 2^(4 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0001));
}
drivenby { // case 289
  x = (true@0b100@0b1010);
  y = (false@0b010@0b1100);
  // x / y
  // -3.2500000 / 0.8750000 = -3.7142856121063232421875
  // (-1)^(1) * 2^(4 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1110));
}
drivenby { // case 290
  x = (true@0b000@0b1001);
  y = (false@0b001@0b0111);
  // x / y
  // -0.1406250 / 0.3593750 = -0.3913043439388275146484
  // (-1)^(1) * 2^(1 - 3) * 11001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1001));
}
drivenby { // case 291
  x = (false@0b010@0b0010);
  y = (false@0b001@0b0001);
  // x / y
  // 0.5625000 / 0.2656250 = 2.1176471710205078125000
  // (-1)^(0) * 2^(4 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0001));
}
drivenby { // case 292
  x = (true@0b100@0b0110);
  y = (true@0b001@0b0110);
  // x / y
  // -2.7500000 / -0.3437500 = 8.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0000));
}
drivenby { // case 293
  x = (false@0b100@0b0011);
  y = (true@0b000@0b1111);
  // x / y
  // 2.3750000 / -0.2343750 = -10.1333332061767578125000
  // (-1)^(1) * 2^(6 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b0100));
}
drivenby { // case 294
  x = (true@0b001@0b1011);
  y = (true@0b010@0b1001);
  // x / y
  // -0.4218750 / -0.7812500 = 0.5400000214576721191406
  // (-1)^(0) * 2^(2 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0001));
}
drivenby { // case 295
  x = (true@0b001@0b0011);
  y = (true@0b001@0b0110);
  // x / y
  // -0.2968750 / -0.3437500 = 0.8636363744735717773438
  // (-1)^(0) * 2^(2 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 296
  x = (false@0b001@0b1010);
  y = (true@0b000@0b0111);
  // x / y
  // 0.4062500 / -0.1093750 = -3.7142856121063232421875
  // (-1)^(1) * 2^(4 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1110));
}
drivenby { // case 297
  x = (false@0b001@0b1111);
  y = (true@0b011@0b1100);
  // x / y
  // 0.4843750 / -1.7500000 = -0.2767857015132904052734
  // (-1)^(1) * 2^(1 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0010));
}
drivenby { // case 298
  x = (true@0b101@0b0001);
  y = (false@0b010@0b0011);
  // x / y
  // -4.2500000 / 0.5937500 = -7.1578946113586425781250
  // (-1)^(1) * 2^(5 - 3) * 11100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1101));
}
drivenby { // case 299
  x = (true@0b000@0b1010);
  y = (false@0b011@0b0100);
  // x / y
  // -0.1562500 / 1.2500000 = -0.1250000000000000000000
  // (-1)^(1) * 2^(0 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 300
  x = (true@0b011@0b1000);
  y = (true@0b100@0b1111);
  // x / y
  // -1.5000000 / -3.8750000 = 0.3870967626571655273438
  // (-1)^(0) * 2^(1 - 3) * 11000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1001));
}
drivenby { // case 301
  x = (true@0b010@0b0001);
  y = (false@0b011@0b0001);
  // x / y
  // -0.5312500 / 1.0625000 = -0.5000000000000000000000
  // (-1)^(1) * 2^(2 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0000));
}
drivenby { // case 302
  x = (true@0b010@0b1100);
  y = (true@0b001@0b1101);
  // x / y
  // -0.8750000 / -0.4531250 = 1.9310344457626342773438
  // (-1)^(0) * 2^(3 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 303
  x = (true@0b000@0b1110);
  y = (false@0b011@0b1111);
  // x / y
  // -0.2187500 / 1.9375000 = -0.1129032224416732788086
  // (-1)^(1) * 2^(-1 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0111));
}
drivenby { // case 304
  x = (true@0b000@0b1100);
  y = (false@0b001@0b0100);
  // x / y
  // -0.1875000 / 0.3125000 = -0.6000000238418579101562
  // (-1)^(1) * 2^(2 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0011));
}
drivenby { // case 305
  x = (false@0b010@0b1101);
  y = (false@0b011@0b0111);
  // x / y
  // 0.9062500 / 1.4375000 = 0.6304348111152648925781
  // (-1)^(0) * 2^(2 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0100));
}
drivenby { // case 306
  x = (false@0b011@0b1010);
  y = (true@0b001@0b0111);
  // x / y
  // 1.6250000 / -0.3593750 = -4.5217390060424804687500
  // (-1)^(1) * 2^(5 - 3) * 10010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0010));
}
drivenby { // case 307
  x = (false@0b010@0b0001);
  y = (false@0b101@0b1110);
  // x / y
  // 0.5312500 / 7.5000000 = 0.0708333328366279602051
  // (-1)^(0) * 2^(-1 - 3) * 10010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0100));
}
drivenby { // case 308
  x = (false@0b001@0b0101);
  y = (false@0b001@0b1000);
  // x / y
  // 0.3281250 / 0.3750000 = 0.8750000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 309
  x = (true@0b101@0b0110);
  y = (false@0b001@0b1011);
  // x / y
  // -5.5000000 / 0.4218750 = -13.0370368957519531250000
  // (-1)^(1) * 2^(6 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b1010));
}
drivenby { // case 310
  x = (true@0b101@0b0000);
  y = (false@0b100@0b0111);
  // x / y
  // -4.0000000 / 2.8750000 = -1.3913043737411499023438
  // (-1)^(1) * 2^(3 - 3) * 10110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0110));
}
drivenby { // case 311
  x = (false@0b100@0b1000);
  y = (false@0b001@0b1101);
  // x / y
  // 3.0000000 / 0.4531250 = 6.6206898689270019531250
  // (-1)^(0) * 2^(5 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1010));
}
drivenby { // case 312
  x = (true@0b001@0b0110);
  y = (true@0b011@0b0001);
  // x / y
  // -0.3437500 / -1.0625000 = 0.3235294222831726074219
  // (-1)^(0) * 2^(1 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0101));
}
drivenby { // case 313
  x = (true@0b011@0b1100);
  y = (false@0b000@0b1100);
  // x / y
  // -1.7500000 / 0.1875000 = -9.3333330154418945312500
  // (-1)^(1) * 2^(6 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b110@0b0011));
}
drivenby { // case 314
  x = (false@0b001@0b0111);
  y = (true@0b100@0b1110);
  // x / y
  // 0.3593750 / -3.7500000 = -0.0958333313465118408203
  // (-1)^(1) * 2^(-1 - 3) * 11000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 315
  x = (false@0b101@0b0001);
  y = (false@0b101@0b1001);
  // x / y
  // 4.2500000 / 6.2500000 = 0.6800000071525573730469
  // (-1)^(0) * 2^(2 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0110));
}
drivenby { // case 316
  x = (false@0b011@0b0101);
  y = (false@0b001@0b0110);
  // x / y
  // 1.3125000 / 0.3437500 = 3.8181817531585693359375
  // (-1)^(0) * 2^(4 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1111));
}
drivenby { // case 317
  x = (false@0b101@0b1101);
  y = (false@0b010@0b0111);
  // x / y
  // 7.2500000 / 0.7187500 = 10.0869569778442382812500
  // (-1)^(0) * 2^(6 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0100));
}
drivenby { // case 318
  x = (true@0b101@0b0000);
  y = (false@0b010@0b0110);
  // x / y
  // -4.0000000 / 0.6875000 = -5.8181819915771484375000
  // (-1)^(1) * 2^(5 - 3) * 10111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0111));
}
drivenby { // case 319
  x = (false@0b000@0b0100);
  y = (true@0b101@0b1110);
  // x / y
  // 0.0625000 / -7.5000000 = -0.0083333337679505348206
  // (-1)^(1) * 2^(-4 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0000));
}
drivenby { // case 320
  x = (true@0b000@0b0110);
  y = (false@0b100@0b0010);
  // x / y
  // -0.0937500 / 2.2500000 = -0.0416666679084300994873
  // (-1)^(1) * 2^(-2 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 321
  x = (false@0b010@0b0110);
  y = (true@0b001@0b0001);
  // x / y
  // 0.6875000 / -0.2656250 = -2.5882353782653808593750
  // (-1)^(1) * 2^(4 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0101));
}
drivenby { // case 322
  x = (false@0b011@0b1100);
  y = (true@0b101@0b1000);
  // x / y
  // 1.7500000 / -6.0000000 = -0.2916666567325592041016
  // (-1)^(1) * 2^(1 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0011));
}
drivenby { // case 323
  x = (false@0b100@0b0100);
  y = (true@0b100@0b0100);
  // x / y
  // 2.5000000 / -2.5000000 = -1.0000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0000));
}
drivenby { // case 324
  x = (true@0b010@0b0000);
  y = (true@0b101@0b0000);
  // x / y
  // -0.5000000 / -4.0000000 = 0.1250000000000000000000
  // (-1)^(0) * 2^(0 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1000));
}
drivenby { // case 325
  x = (true@0b010@0b1110);
  y = (false@0b101@0b1010);
  // x / y
  // -0.9375000 / 6.5000000 = -0.1442307680845260620117
  // (-1)^(1) * 2^(0 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 326
  x = (true@0b011@0b1101);
  y = (true@0b010@0b1110);
  // x / y
  // -1.8125000 / -0.9375000 = 1.9333332777023315429688
  // (-1)^(0) * 2^(3 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 327
  x = (false@0b000@0b1101);
  y = (true@0b000@0b1101);
  // x / y
  // 0.2031250 / -0.2031250 = -1.0000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0000));
}
drivenby { // case 328
  x = (true@0b100@0b1100);
  y = (true@0b011@0b1111);
  // x / y
  // -3.5000000 / -1.9375000 = 1.8064515590667724609375
  // (-1)^(0) * 2^(3 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1101));
}
drivenby { // case 329
  x = (false@0b010@0b1001);
  y = (false@0b000@0b1111);
  // x / y
  // 0.7812500 / 0.2343750 = 3.3333332538604736328125
  // (-1)^(0) * 2^(4 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1011));
}
drivenby { // case 330
  x = (false@0b001@0b1011);
  y = (true@0b010@0b0110);
  // x / y
  // 0.4218750 / -0.6875000 = -0.6136363744735717773438
  // (-1)^(1) * 2^(2 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0100));
}
drivenby { // case 331
  x = (true@0b001@0b0100);
  y = (false@0b100@0b0100);
  // x / y
  // -0.3125000 / 2.5000000 = -0.1250000000000000000000
  // (-1)^(1) * 2^(0 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 332
  x = (false@0b101@0b1101);
  y = (true@0b101@0b1110);
  // x / y
  // 7.2500000 / -7.5000000 = -0.9666666388511657714844
  // (-1)^(1) * 2^(2 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1111));
}
drivenby { // case 333
  x = (false@0b100@0b1111);
  y = (true@0b010@0b1000);
  // x / y
  // 3.8750000 / -0.7500000 = -5.1666665077209472656250
  // (-1)^(1) * 2^(5 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0101));
}
drivenby { // case 334
  x = (false@0b000@0b0011);
  y = (false@0b010@0b0110);
  // x / y
  // 0.0468750 / 0.6875000 = 0.0681818202137947082520
  // (-1)^(0) * 2^(-1 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0100));
}
drivenby { // case 335
  x = (false@0b101@0b1100);
  y = (false@0b010@0b1100);
  // x / y
  // 7.0000000 / 0.8750000 = 8.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0000));
}
drivenby { // case 336
  x = (false@0b100@0b1001);
  y = (false@0b100@0b1111);
  // x / y
  // 3.1250000 / 3.8750000 = 0.8064516186714172363281
  // (-1)^(0) * 2^(2 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1010));
}
drivenby { // case 337
  x = (true@0b001@0b0111);
  y = (false@0b100@0b0100);
  // x / y
  // -0.3593750 / 2.5000000 = -0.1437499970197677612305
  // (-1)^(1) * 2^(0 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 338
  x = (false@0b000@0b0101);
  y = (false@0b011@0b1011);
  // x / y
  // 0.0781250 / 1.6875000 = 0.0462962947785854339600
  // (-1)^(0) * 2^(-2 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 339
  x = (false@0b100@0b0101);
  y = (false@0b010@0b1000);
  // x / y
  // 2.6250000 / 0.7500000 = 3.5000000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1100));
}
drivenby { // case 340
  x = (true@0b100@0b0011);
  y = (false@0b101@0b1110);
  // x / y
  // -2.3750000 / 7.5000000 = -0.3166666626930236816406
  // (-1)^(1) * 2^(1 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0100));
}
drivenby { // case 341
  x = (false@0b000@0b1101);
  y = (true@0b100@0b0111);
  // x / y
  // 0.2031250 / -2.8750000 = -0.0706521719694137573242
  // (-1)^(1) * 2^(-1 - 3) * 10010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 342
  x = (true@0b010@0b0001);
  y = (true@0b100@0b0010);
  // x / y
  // -0.5312500 / -2.2500000 = 0.2361111044883728027344
  // (-1)^(0) * 2^(0 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1111));
}
drivenby { // case 343
  x = (false@0b010@0b1110);
  y = (false@0b010@0b1110);
  // x / y
  // 0.9375000 / 0.9375000 = 1.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0000));
}
drivenby { // case 344
  x = (false@0b101@0b0001);
  y = (true@0b101@0b0001);
  // x / y
  // 4.2500000 / -4.2500000 = -1.0000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0000));
}
drivenby { // case 345
  x = (false@0b100@0b0110);
  y = (false@0b011@0b0011);
  // x / y
  // 2.7500000 / 1.1875000 = 2.3157894611358642578125
  // (-1)^(0) * 2^(4 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0011));
}
drivenby { // case 346
  x = (false@0b011@0b1101);
  y = (true@0b100@0b0010);
  // x / y
  // 1.8125000 / -2.2500000 = -0.8055555820465087890625
  // (-1)^(1) * 2^(2 - 3) * 11001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 347
  x = (true@0b001@0b0110);
  y = (false@0b001@0b0001);
  // x / y
  // -0.3437500 / 0.2656250 = -1.2941176891326904296875
  // (-1)^(1) * 2^(3 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0101));
}
drivenby { // case 348
  x = (false@0b101@0b1000);
  y = (true@0b100@0b0111);
  // x / y
  // 6.0000000 / -2.8750000 = -2.0869565010070800781250
  // (-1)^(1) * 2^(4 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0001));
}
drivenby { // case 349
  x = (true@0b010@0b1100);
  y = (true@0b000@0b0111);
  // x / y
  // -0.8750000 / -0.1093750 = 8.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b0000));
}
drivenby { // case 350
  x = (false@0b000@0b1000);
  y = (true@0b011@0b0110);
  // x / y
  // 0.1250000 / -1.3750000 = -0.0909090936183929443359
  // (-1)^(1) * 2^(-1 - 3) * 10111 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0101));
}
drivenby { // case 351
  x = (false@0b001@0b0101);
  y = (true@0b000@0b1011);
  // x / y
  // 0.3281250 / -0.1718750 = -1.9090908765792846679688
  // (-1)^(1) * 2^(3 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 352
  x = (true@0b010@0b1000);
  y = (false@0b010@0b1101);
  // x / y
  // -0.7500000 / 0.9062500 = -0.8275862336158752441406
  // (-1)^(1) * 2^(2 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 353
  x = (true@0b000@0b1111);
  y = (true@0b000@0b0100);
  // x / y
  // -0.2343750 / -0.0625000 = 3.7500000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 11110 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1110));
}
drivenby { // case 354
  x = (false@0b101@0b1101);
  y = (false@0b100@0b1111);
  // x / y
  // 7.2500000 / 3.8750000 = 1.8709677457809448242188
  // (-1)^(0) * 2^(3 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1110));
}
drivenby { // case 355
  x = (true@0b000@0b1111);
  y = (true@0b001@0b0011);
  // x / y
  // -0.2343750 / -0.2968750 = 0.7894737124443054199219
  // (-1)^(0) * 2^(2 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1001));
}
drivenby { // case 356
  x = (true@0b001@0b0111);
  y = (false@0b000@0b1100);
  // x / y
  // -0.3593750 / 0.1875000 = -1.9166666269302368164062
  // (-1)^(1) * 2^(3 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1111));
}
drivenby { // case 357
  x = (false@0b100@0b1101);
  y = (false@0b100@0b0001);
  // x / y
  // 3.6250000 / 2.1250000 = 1.7058823108673095703125
  // (-1)^(0) * 2^(3 - 3) * 11011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1011));
}
drivenby { // case 358
  x = (true@0b010@0b1001);
  y = (false@0b101@0b0011);
  // x / y
  // -0.7812500 / 4.7500000 = -0.1644736826419830322266
  // (-1)^(1) * 2^(0 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1010));
}
drivenby { // case 359
  x = (true@0b100@0b0111);
  y = (true@0b100@0b0010);
  // x / y
  // -2.8750000 / -2.2500000 = 1.2777777910232543945312
  // (-1)^(0) * 2^(3 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 360
  x = (true@0b010@0b1101);
  y = (true@0b100@0b1011);
  // x / y
  // -0.9062500 / -3.3750000 = 0.2685185074806213378906
  // (-1)^(0) * 2^(1 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0001));
}
drivenby { // case 361
  x = (false@0b100@0b1000);
  y = (false@0b001@0b1100);
  // x / y
  // 3.0000000 / 0.4375000 = 6.8571429252624511718750
  // (-1)^(0) * 2^(5 - 3) * 11011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1011));
}
drivenby { // case 362
  x = (false@0b010@0b1111);
  y = (true@0b100@0b1100);
  // x / y
  // 0.9687500 / -3.5000000 = -0.2767857015132904052734
  // (-1)^(1) * 2^(1 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0010));
}
drivenby { // case 363
  x = (false@0b011@0b0010);
  y = (true@0b001@0b0010);
  // x / y
  // 1.1250000 / -0.2812500 = -4.0000000000000000000000
  // (-1)^(1) * 2^(5 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0000));
}
drivenby { // case 364
  x = (true@0b010@0b0010);
  y = (false@0b010@0b0110);
  // x / y
  // -0.5625000 / 0.6875000 = -0.8181818127632141113281
  // (-1)^(1) * 2^(2 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 365
  x = (true@0b011@0b0001);
  y = (true@0b011@0b1000);
  // x / y
  // -1.0625000 / -1.5000000 = 0.7083333134651184082031
  // (-1)^(0) * 2^(2 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0111));
}
drivenby { // case 366
  x = (false@0b100@0b1000);
  y = (true@0b101@0b1110);
  // x / y
  // 3.0000000 / -7.5000000 = -0.4000000059604644775391
  // (-1)^(1) * 2^(1 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1010));
}
drivenby { // case 367
  x = (true@0b000@0b1100);
  y = (true@0b001@0b1000);
  // x / y
  // -0.1875000 / -0.3750000 = 0.5000000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0000));
}
drivenby { // case 368
  x = (false@0b001@0b1110);
  y = (false@0b101@0b0010);
  // x / y
  // 0.4687500 / 4.5000000 = 0.1041666641831398010254
  // (-1)^(0) * 2^(-1 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0110));
}
drivenby { // case 369
  x = (false@0b001@0b1110);
  y = (false@0b011@0b1110);
  // x / y
  // 0.4687500 / 1.8750000 = 0.2500000000000000000000
  // (-1)^(0) * 2^(1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0000));
}
drivenby { // case 370
  x = (false@0b010@0b0101);
  y = (true@0b011@0b0111);
  // x / y
  // 0.6562500 / -1.4375000 = -0.4565217494964599609375
  // (-1)^(1) * 2^(1 - 3) * 11101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1101));
}
drivenby { // case 371
  x = (true@0b001@0b1001);
  y = (true@0b100@0b0100);
  // x / y
  // -0.3906250 / -2.5000000 = 0.1562500000000000000000
  // (-1)^(0) * 2^(0 - 3) * 10100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1010));
}
drivenby { // case 372
  x = (true@0b001@0b1100);
  y = (true@0b011@0b1000);
  // x / y
  // -0.4375000 / -1.5000000 = 0.2916666567325592041016
  // (-1)^(0) * 2^(1 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0011));
}
drivenby { // case 373
  x = (false@0b011@0b1000);
  y = (false@0b011@0b0001);
  // x / y
  // 1.5000000 / 1.0625000 = 1.4117647409439086914062
  // (-1)^(0) * 2^(3 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0111));
}
drivenby { // case 374
  x = (true@0b001@0b1011);
  y = (false@0b011@0b1110);
  // x / y
  // -0.4218750 / 1.8750000 = -0.2249999940395355224609
  // (-1)^(1) * 2^(0 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1110));
}
drivenby { // case 375
  x = (true@0b001@0b0110);
  y = (true@0b100@0b1001);
  // x / y
  // -0.3437500 / -3.1250000 = 0.1099999994039535522461
  // (-1)^(0) * 2^(-1 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0111));
}
drivenby { // case 376
  x = (true@0b010@0b0010);
  y = (false@0b010@0b0011);
  // x / y
  // -0.5625000 / 0.5937500 = -0.9473684430122375488281
  // (-1)^(1) * 2^(2 - 3) * 11110 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1110));
}
drivenby { // case 377
  x = (true@0b000@0b0001);
  y = (true@0b001@0b0101);
  // x / y
  // -0.0156250 / -0.3281250 = 0.0476190485060214996338
  // (-1)^(0) * 2^(-2 - 3) * 11000 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 378
  x = (false@0b010@0b0110);
  y = (true@0b010@0b0111);
  // x / y
  // 0.6875000 / -0.7187500 = -0.9565217494964599609375
  // (-1)^(1) * 2^(2 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1111));
}
drivenby { // case 379
  x = (true@0b100@0b0000);
  y = (true@0b010@0b1000);
  // x / y
  // -2.0000000 / -0.7500000 = 2.6666667461395263671875
  // (-1)^(0) * 2^(4 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 380
  x = (false@0b011@0b1101);
  y = (false@0b101@0b1010);
  // x / y
  // 1.8125000 / 6.5000000 = 0.2788461446762084960938
  // (-1)^(0) * 2^(1 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0010));
}
drivenby { // case 381
  x = (true@0b010@0b0110);
  y = (true@0b001@0b0000);
  // x / y
  // -0.6875000 / -0.2500000 = 2.7500000000000000000000
  // (-1)^(0) * 2^(4 - 3) * 10110 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0110));
}
drivenby { // case 382
  x = (false@0b000@0b0101);
  y = (false@0b101@0b0011);
  // x / y
  // 0.0781250 / 4.7500000 = 0.0164473690092563629150
  // (-1)^(0) * 2^(-3 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0001));
}
drivenby { // case 383
  x = (true@0b001@0b1001);
  y = (true@0b010@0b0010);
  // x / y
  // -0.3906250 / -0.5625000 = 0.6944444179534912109375
  // (-1)^(0) * 2^(2 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0110));
}
drivenby { // case 384
  x = (true@0b001@0b0100);
  y = (true@0b011@0b1000);
  // x / y
  // -0.3125000 / -1.5000000 = 0.2083333283662796020508
  // (-1)^(0) * 2^(0 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1101));
}
drivenby { // case 385
  x = (true@0b011@0b0100);
  y = (false@0b011@0b0011);
  // x / y
  // -1.2500000 / 1.1875000 = -1.0526316165924072265625
  // (-1)^(1) * 2^(3 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0001));
}
drivenby { // case 386
  x = (false@0b000@0b1110);
  y = (false@0b011@0b1100);
  // x / y
  // 0.2187500 / 1.7500000 = 0.1250000000000000000000
  // (-1)^(0) * 2^(0 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1000));
}
drivenby { // case 387
  x = (false@0b001@0b0100);
  y = (true@0b011@0b1101);
  // x / y
  // 0.3125000 / -1.8125000 = -0.1724137961864471435547
  // (-1)^(1) * 2^(0 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1011));
}
drivenby { // case 388
  x = (false@0b100@0b1000);
  y = (false@0b101@0b0000);
  // x / y
  // 3.0000000 / 4.0000000 = 0.7500000000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1000));
}
drivenby { // case 389
  x = (false@0b100@0b0100);
  y = (false@0b001@0b1011);
  // x / y
  // 2.5000000 / 0.4218750 = 5.9259257316589355468750
  // (-1)^(0) * 2^(5 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1000));
}
drivenby { // case 390
  x = (false@0b010@0b1100);
  y = (false@0b011@0b1101);
  // x / y
  // 0.8750000 / 1.8125000 = 0.4827586114406585693359
  // (-1)^(0) * 2^(1 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1111));
}
drivenby { // case 391
  x = (true@0b001@0b0111);
  y = (true@0b010@0b1100);
  // x / y
  // -0.3593750 / -0.8750000 = 0.4107142984867095947266
  // (-1)^(0) * 2^(1 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b1010));
}
drivenby { // case 392
  x = (true@0b100@0b1111);
  y = (false@0b011@0b0010);
  // x / y
  // -3.8750000 / 1.1250000 = -3.4444444179534912109375
  // (-1)^(1) * 2^(4 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b1100));
}
drivenby { // case 393
  x = (true@0b000@0b0101);
  y = (false@0b100@0b1101);
  // x / y
  // -0.0781250 / 3.6250000 = -0.0215517245233058929443
  // (-1)^(1) * 2^(-3 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0001));
}
drivenby { // case 394
  x = (false@0b010@0b0100);
  y = (false@0b010@0b1101);
  // x / y
  // 0.6250000 / 0.9062500 = 0.6896551847457885742188
  // (-1)^(0) * 2^(2 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0110));
}
drivenby { // case 395
  x = (true@0b100@0b0010);
  y = (true@0b001@0b1111);
  // x / y
  // -2.2500000 / -0.4843750 = 4.6451611518859863281250
  // (-1)^(0) * 2^(5 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0011));
}
drivenby { // case 396
  x = (false@0b010@0b1110);
  y = (true@0b101@0b0110);
  // x / y
  // 0.9375000 / -5.5000000 = -0.1704545468091964721680
  // (-1)^(1) * 2^(0 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1011));
}
drivenby { // case 397
  x = (true@0b001@0b0111);
  y = (false@0b101@0b1010);
  // x / y
  // -0.3593750 / 6.5000000 = -0.0552884601056575775146
  // (-1)^(1) * 2^(-2 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0011));
}
drivenby { // case 398
  x = (false@0b000@0b0010);
  y = (false@0b010@0b1110);
  // x / y
  // 0.0312500 / 0.9375000 = 0.0333333350718021392822
  // (-1)^(0) * 2^(-2 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0010));
}
drivenby { // case 399
  x = (false@0b001@0b1010);
  y = (false@0b001@0b1100);
  // x / y
  // 0.4062500 / 0.4375000 = 0.9285714030265808105469
  // (-1)^(0) * 2^(2 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1110));
}
drivenby { // case 400
  x = (true@0b011@0b1101);
  y = (true@0b100@0b0000);
  // x / y
  // -1.8125000 / -2.0000000 = 0.9062500000000000000000
  // (-1)^(0) * 2^(2 - 3) * 11101 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1101));
}
drivenby { // case 401
  x = (false@0b001@0b1000);
  y = (true@0b000@0b1010);
  // x / y
  // 0.3750000 / -0.1562500 = -2.4000000953674316406250
  // (-1)^(1) * 2^(4 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0011));
}
drivenby { // case 402
  x = (true@0b000@0b0111);
  y = (false@0b000@0b1111);
  // x / y
  // -0.1093750 / 0.2343750 = -0.4666666686534881591797
  // (-1)^(1) * 2^(1 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1110));
}
drivenby { // case 403
  x = (true@0b001@0b1110);
  y = (true@0b001@0b1001);
  // x / y
  // -0.4687500 / -0.3906250 = 1.2000000476837158203125
  // (-1)^(0) * 2^(3 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 404
  x = (false@0b101@0b1110);
  y = (false@0b101@0b0001);
  // x / y
  // 7.5000000 / 4.2500000 = 1.7647058963775634765625
  // (-1)^(0) * 2^(3 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1100));
}
drivenby { // case 405
  x = (true@0b001@0b1110);
  y = (false@0b010@0b0001);
  // x / y
  // -0.4687500 / 0.5312500 = -0.8823529481887817382812
  // (-1)^(1) * 2^(2 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1100));
}
drivenby { // case 406
  x = (false@0b011@0b0110);
  y = (false@0b010@0b0100);
  // x / y
  // 1.3750000 / 0.6250000 = 2.2000000476837158203125
  // (-1)^(0) * 2^(4 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0010));
}
drivenby { // case 407
  x = (false@0b011@0b1000);
  y = (true@0b010@0b0001);
  // x / y
  // 1.5000000 / -0.5312500 = -2.8235294818878173828125
  // (-1)^(1) * 2^(4 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0111));
}
drivenby { // case 408
  x = (true@0b011@0b0000);
  y = (false@0b010@0b1111);
  // x / y
  // -1.0000000 / 0.9687500 = -1.0322580337524414062500
  // (-1)^(1) * 2^(3 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0001));
}
drivenby { // case 409
  x = (true@0b100@0b1101);
  y = (true@0b101@0b1100);
  // x / y
  // -3.6250000 / -7.0000000 = 0.5178571343421936035156
  // (-1)^(0) * 2^(2 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0001));
}
drivenby { // case 410
  x = (false@0b000@0b0110);
  y = (false@0b010@0b1101);
  // x / y
  // 0.0937500 / 0.9062500 = 0.1034482792019844055176
  // (-1)^(0) * 2^(-1 - 3) * 11010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0110));
}
drivenby { // case 411
  x = (false@0b101@0b0010);
  y = (true@0b010@0b0100);
  // x / y
  // 4.5000000 / -0.6250000 = -7.1999998092651367187500
  // (-1)^(1) * 2^(5 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1101));
}
drivenby { // case 412
  x = (true@0b001@0b0000);
  y = (false@0b010@0b0011);
  // x / y
  // -0.2500000 / 0.5937500 = -0.4210526347160339355469
  // (-1)^(1) * 2^(1 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1011));
}
drivenby { // case 413
  x = (true@0b010@0b0111);
  y = (false@0b001@0b1001);
  // x / y
  // -0.7187500 / 0.3906250 = -1.8400000333786010742188
  // (-1)^(1) * 2^(3 - 3) * 11101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1101));
}
drivenby { // case 414
  x = (false@0b001@0b1001);
  y = (true@0b101@0b0000);
  // x / y
  // 0.3906250 / -4.0000000 = -0.0976562500000000000000
  // (-1)^(1) * 2^(-1 - 3) * 11001 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0110));
}
drivenby { // case 415
  x = (false@0b000@0b0000);
  y = (true@0b001@0b1011);
  // x / y
  // 0.0000000 / -0.4218750 = -0.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 00000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0000));
}
drivenby { // case 416
  x = (true@0b001@0b1101);
  y = (true@0b011@0b0101);
  // x / y
  // -0.4531250 / -1.3125000 = 0.3452380895614624023438
  // (-1)^(0) * 2^(1 - 3) * 10110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0110));
}
drivenby { // case 417
  x = (true@0b100@0b1100);
  y = (true@0b001@0b0000);
  // x / y
  // -3.5000000 / -0.2500000 = 14.0000000000000000000000
  // (-1)^(0) * 2^(6 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b110@0b1100));
}
drivenby { // case 418
  x = (true@0b000@0b1001);
  y = (false@0b100@0b0010);
  // x / y
  // -0.1406250 / 2.2500000 = -0.0625000000000000000000
  // (-1)^(1) * 2^(-1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 419
  x = (false@0b011@0b0000);
  y = (true@0b100@0b0001);
  // x / y
  // 1.0000000 / -2.1250000 = -0.4705882370471954345703
  // (-1)^(1) * 2^(1 - 3) * 11110 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1110));
}
drivenby { // case 420
  x = (true@0b011@0b1011);
  y = (false@0b010@0b0110);
  // x / y
  // -1.6875000 / 0.6875000 = -2.4545454978942871093750
  // (-1)^(1) * 2^(4 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0100));
}
drivenby { // case 421
  x = (false@0b001@0b0011);
  y = (true@0b100@0b0010);
  // x / y
  // 0.2968750 / -2.2500000 = -0.1319444477558135986328
  // (-1)^(1) * 2^(0 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1000));
}
drivenby { // case 422
  x = (true@0b001@0b0011);
  y = (true@0b101@0b0010);
  // x / y
  // -0.2968750 / -4.5000000 = 0.0659722238779067993164
  // (-1)^(0) * 2^(-1 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0100));
}
drivenby { // case 423
  x = (true@0b000@0b1111);
  y = (true@0b100@0b0010);
  // x / y
  // -0.2343750 / -2.2500000 = 0.1041666641831398010254
  // (-1)^(0) * 2^(-1 - 3) * 11010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0110));
}
drivenby { // case 424
  x = (true@0b011@0b0001);
  y = (false@0b100@0b1111);
  // x / y
  // -1.0625000 / 3.8750000 = -0.2741935551166534423828
  // (-1)^(1) * 2^(1 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0010));
}
drivenby { // case 425
  x = (true@0b100@0b0000);
  y = (false@0b011@0b0011);
  // x / y
  // -2.0000000 / 1.1875000 = -1.6842105388641357421875
  // (-1)^(1) * 2^(3 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1011));
}
drivenby { // case 426
  x = (true@0b100@0b1000);
  y = (false@0b010@0b0001);
  // x / y
  // -3.0000000 / 0.5312500 = -5.6470589637756347656250
  // (-1)^(1) * 2^(5 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b0111));
}
drivenby { // case 427
  x = (false@0b010@0b0001);
  y = (false@0b011@0b0000);
  // x / y
  // 0.5312500 / 1.0000000 = 0.5312500000000000000000
  // (-1)^(0) * 2^(2 - 3) * 10001 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0001));
}
drivenby { // case 428
  x = (false@0b000@0b0011);
  y = (false@0b100@0b1110);
  // x / y
  // 0.0468750 / 3.7500000 = 0.0125000001862645149231
  // (-1)^(0) * 2^(-4 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 429
  x = (false@0b001@0b1000);
  y = (true@0b011@0b0100);
  // x / y
  // 0.3750000 / -1.2500000 = -0.3000000119209289550781
  // (-1)^(1) * 2^(1 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0011));
}
drivenby { // case 430
  x = (false@0b010@0b1110);
  y = (false@0b011@0b0011);
  // x / y
  // 0.9375000 / 1.1875000 = 0.7894737124443054199219
  // (-1)^(0) * 2^(2 - 3) * 11001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1001));
}
drivenby { // case 431
  x = (true@0b000@0b1101);
  y = (false@0b100@0b1110);
  // x / y
  // -0.2031250 / 3.7500000 = -0.0541666671633720397949
  // (-1)^(1) * 2^(-2 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0011));
}
drivenby { // case 432
  x = (true@0b010@0b0000);
  y = (true@0b100@0b0011);
  // x / y
  // -0.5000000 / -2.3750000 = 0.2105263173580169677734
  // (-1)^(0) * 2^(0 - 3) * 11010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1101));
}
drivenby { // case 433
  x = (true@0b100@0b1001);
  y = (true@0b100@0b0011);
  // x / y
  // -3.1250000 / -2.3750000 = 1.3157894611358642578125
  // (-1)^(0) * 2^(3 - 3) * 10101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0101));
}
drivenby { // case 434
  x = (false@0b000@0b0001);
  y = (false@0b001@0b0010);
  // x / y
  // 0.0156250 / 0.2812500 = 0.0555555559694766998291
  // (-1)^(0) * 2^(-2 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0011));
}
drivenby { // case 435
  x = (false@0b101@0b1000);
  y = (false@0b100@0b1001);
  // x / y
  // 6.0000000 / 3.1250000 = 1.9199999570846557617188
  // (-1)^(0) * 2^(3 - 3) * 11110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1111));
}
drivenby { // case 436
  x = (true@0b011@0b0111);
  y = (true@0b001@0b0101);
  // x / y
  // -1.4375000 / -0.3281250 = 4.3809523582458496093750
  // (-1)^(0) * 2^(5 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0010));
}
drivenby { // case 437
  x = (true@0b001@0b0101);
  y = (true@0b100@0b0011);
  // x / y
  // -0.3281250 / -2.3750000 = 0.1381578892469406127930
  // (-1)^(0) * 2^(0 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b1001));
}
drivenby { // case 438
  x = (false@0b011@0b1100);
  y = (false@0b010@0b1110);
  // x / y
  // 1.7500000 / 0.9375000 = 1.8666666746139526367188
  // (-1)^(0) * 2^(3 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1110));
}
drivenby { // case 439
  x = (true@0b000@0b0110);
  y = (false@0b000@0b0100);
  // x / y
  // -0.0937500 / 0.0625000 = -1.5000000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b1000));
}
drivenby { // case 440
  x = (false@0b000@0b0000);
  y = (false@0b100@0b0100);
  // x / y
  // 0.0000000 / 2.5000000 = 0.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 00000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 441
  x = (false@0b000@0b1011);
  y = (true@0b011@0b0011);
  // x / y
  // 0.1718750 / -1.1875000 = -0.1447368413209915161133
  // (-1)^(1) * 2^(0 - 3) * 10010 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 442
  x = (true@0b101@0b1000);
  y = (false@0b100@0b1000);
  // x / y
  // -6.0000000 / 3.0000000 = -2.0000000000000000000000
  // (-1)^(1) * 2^(4 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0000));
}
drivenby { // case 443
  x = (false@0b011@0b0011);
  y = (false@0b001@0b1111);
  // x / y
  // 1.1875000 / 0.4843750 = 2.4516129493713378906250
  // (-1)^(0) * 2^(4 - 3) * 10011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0100));
}
drivenby { // case 444
  x = (false@0b010@0b1100);
  y = (true@0b000@0b1000);
  // x / y
  // 0.8750000 / -0.1250000 = -7.0000000000000000000000
  // (-1)^(1) * 2^(5 - 3) * 11100 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1100));
}
drivenby { // case 445
  x = (false@0b010@0b0001);
  y = (false@0b001@0b1011);
  // x / y
  // 0.5312500 / 0.4218750 = 1.2592592239379882812500
  // (-1)^(0) * 2^(3 - 3) * 10100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0100));
}
drivenby { // case 446
  x = (false@0b011@0b1000);
  y = (false@0b100@0b0010);
  // x / y
  // 1.5000000 / 2.2500000 = 0.6666666865348815917969
  // (-1)^(0) * 2^(2 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0101));
}
drivenby { // case 447
  x = (false@0b000@0b0010);
  y = (true@0b000@0b0101);
  // x / y
  // 0.0312500 / -0.0781250 = -0.4000000059604644775391
  // (-1)^(1) * 2^(1 - 3) * 11001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1010));
}
drivenby { // case 448
  x = (true@0b100@0b0101);
  y = (true@0b010@0b0111);
  // x / y
  // -2.6250000 / -0.7187500 = 3.6521739959716796875000
  // (-1)^(0) * 2^(4 - 3) * 11101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1101));
}
drivenby { // case 449
  x = (true@0b010@0b0100);
  y = (false@0b100@0b0011);
  // x / y
  // -0.6250000 / 2.3750000 = -0.2631579041481018066406
  // (-1)^(1) * 2^(1 - 3) * 10000 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b0001));
}
drivenby { // case 450
  x = (false@0b000@0b0111);
  y = (true@0b011@0b1100);
  // x / y
  // 0.1093750 / -1.7500000 = -0.0625000000000000000000
  // (-1)^(1) * 2^(-1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 451
  x = (true@0b001@0b0010);
  y = (false@0b010@0b1000);
  // x / y
  // -0.2812500 / 0.7500000 = -0.3750000000000000000000
  // (-1)^(1) * 2^(1 - 3) * 11000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1000));
}
drivenby { // case 452
  x = (true@0b011@0b1010);
  y = (false@0b100@0b0110);
  // x / y
  // -1.6250000 / 2.7500000 = -0.5909090638160705566406
  // (-1)^(1) * 2^(2 - 3) * 10010 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b0011));
}
drivenby { // case 453
  x = (true@0b010@0b0100);
  y = (true@0b000@0b1010);
  // x / y
  // -0.6250000 / -0.1562500 = 4.0000000000000000000000
  // (-1)^(0) * 2^(5 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0000));
}
drivenby { // case 454
  x = (false@0b010@0b1010);
  y = (false@0b010@0b1110);
  // x / y
  // 0.8125000 / 0.9375000 = 0.8666666746139526367188
  // (-1)^(0) * 2^(2 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 455
  x = (true@0b000@0b0001);
  y = (true@0b101@0b1110);
  // x / y
  // -0.0156250 / -7.5000000 = 0.0020833334419876337051
  // (-1)^(0) * 2^(-6 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 456
  x = (true@0b010@0b1011);
  y = (true@0b000@0b1110);
  // x / y
  // -0.8437500 / -0.2187500 = 3.8571429252624511718750
  // (-1)^(0) * 2^(4 - 3) * 11110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1111));
}
drivenby { // case 457
  x = (true@0b101@0b1111);
  y = (true@0b011@0b0010);
  // x / y
  // -7.7500000 / -1.1250000 = 6.8888888359069824218750
  // (-1)^(0) * 2^(5 - 3) * 11011 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1100));
}
drivenby { // case 458
  x = (false@0b101@0b0100);
  y = (false@0b010@0b0110);
  // x / y
  // 5.0000000 / 0.6875000 = 7.2727274894714355468750
  // (-1)^(0) * 2^(5 - 3) * 11101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1101));
}
drivenby { // case 459
  x = (true@0b011@0b0101);
  y = (true@0b101@0b0011);
  // x / y
  // -1.3125000 / -4.7500000 = 0.2763157784938812255859
  // (-1)^(0) * 2^(1 - 3) * 10001 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b001@0b0010));
}
drivenby { // case 460
  x = (true@0b100@0b0011);
  y = (true@0b001@0b1110);
  // x / y
  // -2.3750000 / -0.4687500 = 5.0666666030883789062500
  // (-1)^(0) * 2^(5 - 3) * 10100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0100));
}
drivenby { // case 461
  x = (false@0b100@0b0110);
  y = (true@0b011@0b0001);
  // x / y
  // 2.7500000 / -1.0625000 = -2.5882353782653808593750
  // (-1)^(1) * 2^(4 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0101));
}
drivenby { // case 462
  x = (true@0b010@0b1000);
  y = (true@0b010@0b0010);
  // x / y
  // -0.7500000 / -0.5625000 = 1.3333333730697631835938
  // (-1)^(0) * 2^(3 - 3) * 10101 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0101));
}
drivenby { // case 463
  x = (true@0b100@0b0101);
  y = (true@0b100@0b0101);
  // x / y
  // -2.6250000 / -2.6250000 = 1.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0000));
}
drivenby { // case 464
  x = (true@0b001@0b0110);
  y = (false@0b101@0b0110);
  // x / y
  // -0.3437500 / 5.5000000 = -0.0625000000000000000000
  // (-1)^(1) * 2^(-1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 465
  x = (true@0b000@0b0000);
  y = (true@0b100@0b1010);
  // x / y
  // -0.0000000 / -3.2500000 = 0.0000000000000000000000
  // (-1)^(0) * 2^(3 - 3) * 00000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 466
  x = (true@0b000@0b1110);
  y = (false@0b101@0b1010);
  // x / y
  // -0.2187500 / 6.5000000 = -0.0336538478732109069824
  // (-1)^(1) * 2^(-2 - 3) * 10001 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 467
  x = (true@0b001@0b1010);
  y = (true@0b010@0b1000);
  // x / y
  // -0.4062500 / -0.7500000 = 0.5416666865348815917969
  // (-1)^(0) * 2^(2 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b0001));
}
drivenby { // case 468
  x = (true@0b001@0b1010);
  y = (false@0b100@0b0101);
  // x / y
  // -0.4062500 / 2.6250000 = -0.1547619104385375976562
  // (-1)^(1) * 2^(0 - 3) * 10011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1010));
}
drivenby { // case 469
  x = (false@0b101@0b1100);
  y = (false@0b100@0b1011);
  // x / y
  // 7.0000000 / 3.3750000 = 2.0740740299224853515625
  // (-1)^(0) * 2^(4 - 3) * 10000 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0001));
}
drivenby { // case 470
  x = (true@0b100@0b1110);
  y = (true@0b010@0b0001);
  // x / y
  // -3.7500000 / -0.5312500 = 7.0588235855102539062500
  // (-1)^(0) * 2^(5 - 3) * 11100 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1100));
}
drivenby { // case 471
  x = (true@0b001@0b0010);
  y = (false@0b100@0b0000);
  // x / y
  // -0.2812500 / 2.0000000 = -0.1406250000000000000000
  // (-1)^(1) * 2^(0 - 3) * 10010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1001));
}
drivenby { // case 472
  x = (false@0b000@0b0110);
  y = (true@0b000@0b1110);
  // x / y
  // 0.0937500 / -0.2187500 = -0.4285714328289031982422
  // (-1)^(1) * 2^(1 - 3) * 11011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1011));
}
drivenby { // case 473
  x = (false@0b100@0b0111);
  y = (false@0b001@0b1111);
  // x / y
  // 2.8750000 / 0.4843750 = 5.9354839324951171875000
  // (-1)^(0) * 2^(5 - 3) * 10111 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b1000));
}
drivenby { // case 474
  x = (false@0b001@0b1000);
  y = (false@0b000@0b1011);
  // x / y
  // 0.3750000 / 0.1718750 = 2.1818182468414306640625
  // (-1)^(0) * 2^(4 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0001));
}
drivenby { // case 475
  x = (false@0b001@0b1001);
  y = (false@0b001@0b0101);
  // x / y
  // 0.3906250 / 0.3281250 = 1.1904761791229248046875
  // (-1)^(0) * 2^(3 - 3) * 10011 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0011));
}
drivenby { // case 476
  x = (true@0b000@0b0110);
  y = (false@0b000@0b0011);
  // x / y
  // -0.0937500 / 0.0468750 = -2.0000000000000000000000
  // (-1)^(1) * 2^(4 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0000));
}
drivenby { // case 477
  x = (false@0b011@0b0110);
  y = (false@0b010@0b0001);
  // x / y
  // 1.3750000 / 0.5312500 = 2.5882353782653808593750
  // (-1)^(0) * 2^(4 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0101));
}
drivenby { // case 478
  x = (true@0b000@0b0101);
  y = (false@0b100@0b1100);
  // x / y
  // -0.0781250 / 3.5000000 = -0.0223214291036128997803
  // (-1)^(1) * 2^(-3 - 3) * 10110 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0001));
}
drivenby { // case 479
  x = (true@0b000@0b1101);
  y = (false@0b000@0b0010);
  // x / y
  // -0.2031250 / 0.0312500 = -6.5000000000000000000000
  // (-1)^(1) * 2^(5 - 3) * 11010 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1010));
}
drivenby { // case 480
  x = (true@0b000@0b0011);
  y = (false@0b000@0b1101);
  // x / y
  // -0.0468750 / 0.2031250 = -0.2307692319154739379883
  // (-1)^(1) * 2^(0 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1111));
}
drivenby { // case 481
  x = (true@0b100@0b1101);
  y = (true@0b010@0b1000);
  // x / y
  // -3.6250000 / -0.7500000 = 4.8333334922790527343750
  // (-1)^(0) * 2^(5 - 3) * 10011 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b101@0b0011));
}
drivenby { // case 482
  x = (true@0b100@0b1111);
  y = (false@0b010@0b0001);
  // x / y
  // -3.8750000 / 0.5312500 = -7.2941174507141113281250
  // (-1)^(1) * 2^(5 - 3) * 11101 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b101@0b1101));
}
drivenby { // case 483
  x = (true@0b100@0b1100);
  y = (true@0b010@0b1110);
  // x / y
  // -3.5000000 / -0.9375000 = 3.7333333492279052734375
  // (-1)^(0) * 2^(4 - 3) * 11101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b1110));
}
drivenby { // case 484
  x = (true@0b011@0b0101);
  y = (true@0b001@0b1101);
  // x / y
  // -1.3125000 / -0.4531250 = 2.8965516090393066406250
  // (-1)^(0) * 2^(4 - 3) * 10111 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0111));
}
drivenby { // case 485
  x = (false@0b010@0b1001);
  y = (false@0b001@0b1011);
  // x / y
  // 0.7812500 / 0.4218750 = 1.8518518209457397460938
  // (-1)^(0) * 2^(3 - 3) * 11101 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b1110));
}
drivenby { // case 486
  x = (false@0b000@0b0010);
  y = (true@0b010@0b0000);
  // x / y
  // 0.0312500 / -0.5000000 = -0.0625000000000000000000
  // (-1)^(1) * 2^(-1 - 3) * 10000 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 487
  x = (false@0b011@0b0011);
  y = (false@0b010@0b0001);
  // x / y
  // 1.1875000 / 0.5312500 = 2.2352941036224365234375
  // (-1)^(0) * 2^(4 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b100@0b0010));
}
drivenby { // case 488
  x = (true@0b001@0b0110);
  y = (false@0b001@0b1011);
  // x / y
  // -0.3437500 / 0.4218750 = -0.8148148059844970703125
  // (-1)^(1) * 2^(2 - 3) * 11010 0 0  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b010@0b1010));
}
drivenby { // case 489
  x = (true@0b000@0b0001);
  y = (true@0b011@0b1100);
  // x / y
  // -0.0156250 / -1.7500000 = 0.0089285718277096748352
  // (-1)^(0) * 2^(-4 - 3) * 10010 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b000@0b0000));
}
drivenby { // case 490
  x = (false@0b000@0b1110);
  y = (true@0b010@0b1111);
  // x / y
  // 0.2187500 / -0.9687500 = -0.2258064448833465576172
  // (-1)^(1) * 2^(0 - 3) * 11100 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b1110));
}
drivenby { // case 491
  x = (false@0b001@0b0111);
  y = (false@0b001@0b1010);
  // x / y
  // 0.3593750 / 0.4062500 = 0.8846153616905212402344
  // (-1)^(0) * 2^(2 - 3) * 11100 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b010@0b1100));
}
drivenby { // case 492
  x = (false@0b000@0b1101);
  y = (true@0b101@0b0011);
  // x / y
  // 0.2031250 / -4.7500000 = -0.0427631586790084838867
  // (-1)^(1) * 2^(-2 - 3) * 10101 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0010));
}
drivenby { // case 493
  x = (false@0b100@0b0011);
  y = (false@0b011@0b1011);
  // x / y
  // 2.3750000 / 1.6875000 = 1.4074074029922485351562
  // (-1)^(0) * 2^(3 - 3) * 10110 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(false@0b011@0b0111));
}
drivenby { // case 494
  x = (true@0b010@0b1011);
  y = (false@0b011@0b1111);
  // x / y
  // -0.8437500 / 1.9375000 = -0.4354838728904724121094
  // (-1)^(1) * 2^(1 - 3) * 11011 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b001@0b1100));
}
drivenby { // case 495
  x = (false@0b000@0b0011);
  y = (true@0b010@0b0110);
  // x / y
  // 0.0468750 / -0.6875000 = -0.0681818202137947082520
  // (-1)^(1) * 2^(-1 - 3) * 10001 0 1  (r=false, s=true --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0100));
}
drivenby { // case 496
  x = (true@0b000@0b0101);
  y = (false@0b100@0b1111);
  // x / y
  // -0.0781250 / 3.8750000 = -0.0201612897217273712158
  // (-1)^(1) * 2^(-3 - 3) * 10100 1 0  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b000@0b0001));
}
drivenby { // case 497
  x = (true@0b101@0b1110);
  y = (false@0b100@0b1011);
  // x / y
  // -7.5000000 / 3.3750000 = -2.2222223281860351562500
  // (-1)^(1) * 2^(4 - 3) * 10001 1 1  (r=true, s=true --> round up)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b100@0b0010));
}
drivenby { // case 498
  x = (true@0b010@0b0111);
  y = (false@0b010@0b0000);
  // x / y
  // -0.7187500 / 0.5000000 = -1.4375000000000000000000
  // (-1)^(1) * 2^(3 - 3) * 10111 0 0  (r=false, s=false --> round down)
  immediate abort { await(false); } when (rdy);
  assert(z==(true@0b011@0b0111));
}