Lisp code (s-expression) formatter

Question

jSIMLIB checker prints out s-expression code that is essentially lisp code

(set-option :print-success false) 
(set-logic QF_LIA) 
(declare-fun RETURN () Int)
(declare-fun refs_1_SYMINT () Int)
(declare-fun flags_2_SYMINT () Int)
(assert+ ( and ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 100)) ) ) ( not ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 10)) ) ) ) ) )
(check)
(exit)

How can I format the code, preferable with emacs or TextMate? For example:

(set-option :print-success false) 
(set-logic QF_LIA) 
(declare-fun RETURN () Int)
(declare-fun refs_1_SYMINT () Int)
(declare-fun flags_2_SYMINT () Int)
(assert 
  (and  
    (and 
      (and  
        (distinct  flags_2_SYMINT 0)  
        (=  RETURN flags_2_SYMINT))
      (=  refs_1_SYMINT refs1_1_SYMINT)
      (=  flags_2_SYMINT flags1_2_SYMINT))
    (not 
      (and  
        (distinct  flags_2_SYMINT 0) 
        (=  RETURN flags_2_SYMINT))))) 
(check-sat)

Answer 1

In GNU Emacs you can use indent-pp-sexp.

Set the cursor before the s-expression to pretty-print and type c-u m-x indent-pp-sexp.