diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-19 19:54:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-20 02:54:52 +0000 |
| commit | f91f8f24d6ed98698373f5d51b17cf583adcd768 (patch) | |
| tree | d39cd16afcbbf73e61701a09e049e9d706af49bd /test/regress | |
| parent | a95980ecd80b971086c328c3e1bb731852890a07 (diff) | |
Fix echo printing. (#6573)
Previously, echo surpressed leading, trailing and escape quotes of the
string to print. However, the SMT-LIB standard states that the string is
to be printed as is, including those quote characters.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/echo.smt2 | 18 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fe034c519..8cb7f7d1f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -542,6 +542,7 @@ set(regress_0_tests regress0/define-fun-model.smt2 regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 + regress0/echo.smt2 regress0/eqrange1.smt2 regress0/eqrange2.smt2 regress0/eqrange3.smt2 diff --git a/test/regress/regress0/echo.smt2 b/test/regress/regress0/echo.smt2 new file mode 100644 index 000000000..a2747373e --- /dev/null +++ b/test/regress/regress0/echo.smt2 @@ -0,0 +1,18 @@ +; EXPECT: "str""" +; EXPECT: "str""ing" +; EXPECT: "hi" +; EXPECT: "str""""ing" +; EXPECT: "str""i""ng" +; EXPECT: "str\ing" +; EXPECT: "str\\ing" +; EXPECT: "str\" +; EXPECT: "\u{65}" +(echo "str""") +(echo "str""ing") +(echo "hi") +(echo "str""""ing") +(echo "str""i""ng") +(echo "str\ing") +(echo "str\\ing") +(echo "str\") +(echo "\u{65}") |