summaryrefslogtreecommitdiff
path: root/src/parser/CMakeLists.txt
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-05-13 09:49:33 -0700
committerGitHub <noreply@github.com>2021-05-13 16:49:33 +0000
commit05239e9bdf31d848ff073334d26a790de5412e03 (patch)
treefede281f5c25e7b19d36d91c34f5322d83facaa4 /src/parser/CMakeLists.txt
parent31242de4b423d7225174dd1672edb2dacb68f5b8 (diff)
Always parse streams with line buffer (#6532)
When cvc5 was compiled in competition mode (but not for the application track), then it had a special behavior when reading from stdin. When it received input from stdin, it would read all of stdin and then parse the input as a string because it assumed that the full input is directly available on stdin. However, the non-application tracks of SMT-COMP do not use stdin anymore. They pass a filename to the solver. This special case is not used as a result. Usually, cvc5 parses from stdin using the line buffer, so this commit makes it so that this is always the case, which simplifies the code.
Diffstat (limited to 'src/parser/CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback