diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-02-01 12:40:58 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-01 12:40:58 -0600 |
| commit | a85fec1cc9fc4f42dcfefd8c27171d8ce5647449 (patch) | |
| tree | 4b6820199f4f2763b821de6eda1bfc839448122b /src/smt/command.h | |
| parent | c0937f742479d8a5054e42597da9447d55e876c0 (diff) | |
Avoid calling the printers while converting sexpr to string. (#5842)
This PR modifies sexprToString to use Term::getString to get string constants instead of Term::toString, which depends on the output language. The previous behavior caused CVC4 to crash when AST is picked as the output language.
Diffstat (limited to 'src/smt/command.h')
| -rw-r--r-- | src/smt/command.h | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 9330f2015..a88b7e022 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -51,8 +51,7 @@ class Model; /** * Convert a symbolic expression to string. This method differs from - * Term::toString in that it does not surround constant strings with double - * quote symbols. + * Term::toString in that it does not depend on the output language. * * @param sexpr the symbolic expression to convert * @return the symbolic expression as string |