Notes on implementing the ksmt-solver

In this paper we report on new black-box and white-box approaches implemented in ksmt-solver for checking satisfiability of non-linear constraints over the reals. These approaches are applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and beyond. A prototypical implementation has been evaluated on several non-linear SMT-LIB examples and the results have been compared with state-oftheart SMT solvers.