Logic autodetection is wrong using yices and SReal

[rwbarton]

When I try to solve a problem involving SReal with yices, I get this error from yices:

(error "at line 8, column 19: undefined sort: Real")

From the verbose output:

(set-logic QF_AUFLIA); has algebraic reals, using solver-default logic.

This is wrong of course, since QF_AUFLIA does not include reals at all.

No big deal, since I can just set the logic manually.

[LeventErkok]

Quite right. Unfortunately, selecting a logic is not a straightforward thing to do in SMTLib.. Most solvers are lenient, so we can just not set the logic, and they'll do the right thing. Others, such as CVC4 and Yices, always require fixing the logic. In the CVC4 case, they have a magic ALL_SUPPORTED logic that acts as a fall-back, but not so for Yices. For instance, there doesn't seem to be a combination of Bit-vectors and reals together that we can use for Yices.

In any case, I altered the code so it picks QF_UFLRA for Yices when it detects reals are used; but this isn't guaranteed to work either if you also mix in bit-vectors for the reasons mentioned above. Hopefully this'll be "less incorrect" however. The fallback is always setting it by-hand of course, as you already discovered.

[LeventErkok]

Oh, and I still don't have a full-name for you to put in the ACKS list.. I do appreciate the feedback!