1% When using fallback QE with rlgqe the generic variant of ofsf_cad is is used. 2% However, the code did not care about theories for fallback QE at all, which 3% became apparent with this example. 4 5rlset r; 6 7phi := all(x, ex(y, x^2 + x*y + b > 0 and x + a*y^2 + b <= 0)); 8 9rlgqe phi; 10 11end; 12