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