1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/smt2output.smt2 b/test/regress/regress0/smt2output.smt2
new file mode 100644
index 000000000..26050d931
--- /dev/null
+++ b/test/regress/regress0/smt2output.smt2
@@ -0,0 +1,15 @@
+; This test checks the correct output behavior of SMT-LIBv2 symbols
+; (sometimes they have to be |quoted| with pipes).
+;
+; COMMAND-LINE: -qm
+; EXIT: 10
+(declare-fun |toto| () Bool)
+(declare-fun |to to| () Bool)
+(assert (and toto |to to|))
+(check-sat)
+; EXPECT: sat
+(get-model)
+; EXPECT: (model
+; EXPECT: (define-fun toto () Bool true)
+; EXPECT: (define-fun |to to| () Bool true)
+; EXPECT: )