diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-30 11:05:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-05-30 11:05:42 -0700 |
| commit | be2a85f84fec4e926704f4788c55ec2ba805de39 (patch) | |
| tree | 355f1fdbb6ab858409a324d035fb4faaab4c6b54 /test/regress/regress0 | |
| parent | 60173f62a82b4d71f2fbac51880d44d883ae5109 (diff) | |
Quote symbol when printing empty symbol name (#3025)
When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/printer/empty_symbol_name.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2 new file mode 100644 index 000000000..46652bc24 --- /dev/null +++ b/test/regress/regress0/printer/empty_symbol_name.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +; EXPECT: ((|| (_ bv1 4))) +(set-option :produce-models true) +(set-logic QF_BV) +(declare-const || (_ BitVec 4)) +(assert (= || #b0001)) +(check-sat) +(get-value (||)) |