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
7
8{}
9
10
11phi := all(x, ex(y, x^2 + x*y + b > 0 and x + a*y^2 + b <= 0));
12
13
14                        2                  2
15phi := all x ex y (b + x  + x*y > 0 and a*y  + b + x <= 0)
16
17
18rlgqe phi;
19
20
21{{a <> 0},b > 0 and a <= 0}
22
23
24end;
25
26Tested on x86_64-pc-windows CSL
27Time (counter 1): 31 ms  plus GC time: 63 ms
28
29End of Lisp run after 0.03+0.10 seconds
30real 0.27
31user 0.00
32sys 0.09
33