code: def _get_satisfiability_smt_script(self, constraints=(), variables=()):
          
          smt_script = '(set-logic ALL)\n'
          smt_script += self._smtlib_exprs(variables)
          smt_script += self._smtlib_exprs(constraints)
          smt_script += '(check-sat)\n'
          return smt_script
docs: Returns a SMT script that declare all the symbols and constraint and checks
          their satisfiability (check-sat)
  
          :param extra-constraints: list of extra constraints that we want to evaluate only
                                   in the scope of this call
                                  
          :return string: smt-lib representation of the script that checks the satisfiability