ABSTRACT. The recognition that Symbolic Computation tools could benefit from techniques from the world of Satisability Checking was a primary motivation for the founding of the SC2 community. These benefits could be further demonstrated by the existence of "SMT-like" queries in legacy computer algebra systems; that is, computations which seek to decide satisfiability or identify a satisfying witness.

The Maple CAS has been under continuous development since the 1980s and its core symbolic routines incorporate many heuristics, some of which are "SMT-like". We describe ongoing work to compose an inventory of such "SMT-like" queries extracted from the built-in Maple library, most of which were added long before the inclusion in Maple of explicit software links to SAT/SMT tools. Some of these queries are expressible in the SMT-LIB format using existing logics, and it hoped that an analysis of those that cannot be so expressed could help inform future development of the SMT-LIB standard.