Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Stray lines left in commit #7560

Closed
LeventErkok opened this issue Feb 19, 2025 · 2 comments
Closed

Stray lines left in commit #7560

LeventErkok opened this issue Feb 19, 2025 · 2 comments

Comments

@LeventErkok
Copy link

c2b7b58 seems to have left the following lines in inadvertently:

ctx.regular_stream() << "; (get-info :reason-unknown)\n";
ctx.regular_stream() << "; (get-info :status)\n";
ctx.regular_stream() << "; (get-info :version)\n";
ctx.regular_stream() << "; (get-info :authors)\n";
ctx.regular_stream() << "; (get-info :error-behavior)\n";
ctx.regular_stream() << "; (get-info :parameters)\n";
ctx.regular_stream() << "; (get-info :rlimit)\n";
ctx.regular_stream() << "; (get-info :assertion-stack-levels)\n";

@NikolajBjorner
Copy link
Contributor

this was intended: If you get an unsupported argument to get-info,
then have z3 print back, but commented, set of possible get-info.
Is there any other way you prefer such information?
A rationale for the format was that tools that read output should be able to read comments.

@LeventErkok
Copy link
Author

Ah I see.

Sure, no problem. It just looked weird, but not a big deal. (Perhaps add a line that says ; Allowed get-info parameters: to start the output?) Otherwise it looks rather weird.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants