test/regress/regress0/smt2output.smt2

   1 ; This test checks the correct output behavior of SMT-LIBv2 symbols
   2 ; (sometimes they have to be |quoted| with pipes).
   3 ;
   4 ; COMMAND-LINE: -qm
   5 (declare-fun |toto| () Bool)
   6 (declare-fun |to to| () Bool)
   7 (assert (and toto |to to|))
   8 (check-sat)
   9 ; EXPECT: sat
  10 (get-model)
  11 ; EXPECT: (model
  12 ; EXPECT: (define-fun toto () Bool true)
  13 ; EXPECT: (define-fun |to to| () Bool true)
  14 ; EXPECT: )