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