  ksmt is a CDCL-style calculus for solving non-linear constraints over real
numbers involving polynomials and transcendental functions.
  In this paper we investigate properties of the ksmt calculus and show that it
is a $\delta$-complete decision procedure for bounded problems.
  We also propose an extension with local linearisations, which allow for more
efficient treatment of non-linear constraints.
