Macro test_all 

macro_rules! test_all {
    ($solver:expr,
     $assumps:expr,
     $r1:expr,
     $r0:expr ) => { ... };
    ($solver:expr,
     $assumps:expr,
     $r11:expr,
     $r10:expr,
     $r01:expr,
     $r00:expr ) => { ... };
    ($solver:expr,
     $assumps:expr,
     $r111:expr,
     $r110:expr,
     $r101:expr,
     $r100:expr,
     $r011:expr,
     $r010:expr,
     $r001:expr,
     $r000:expr ) => { ... };
    ($solver:expr,
     $assumps:expr,
     $r1111:expr,
     $r1110:expr,
     $r1101:expr,
     $r1100:expr,
     $r1011:expr,
     $r1010:expr,
     $r1001:expr,
     $r1000:expr,
     $r0111:expr,
     $r0110:expr,
     $r0101:expr,
     $r0100:expr,
     $r0011:expr,
     $r0010:expr,
     $r0001:expr,
     $r0000:expr ) => { ... };
}

Test a solver under given assumptions while iterating through all possible assignments of the first 1-4 variables. This is used in the integration tests.