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

Flush the trace stream before displaying sat results #6162

Merged
merged 1 commit into from
Jul 14, 2022

Conversation

utaal
Copy link
Contributor

@utaal utaal commented Jul 14, 2022

The trace stream can be set to log quantifier instantiations with (set-option :trace true), (set-option :trace-file-name <filename>).

We use the log to profile quantifier instantiations in our verification tool: we use z3's smtlib interface interactively, and we inspect the log after a check-sat returns. Because the trace stream writer is buffered, we witness a partial log of the instantiations if we read it after a sat result is returned but before terminating z3 (we run additional queries on the same z3 process).

This change flushes the trace stream just before reporting a sat result. This seems minimally invasive, but there may be other ways to achieve a similar result that you may prefer, such as adding a new command to flush the trace stream. We could also make this configurable with an additional :trace option.

/cc @parno @Chris-Hawblitzel

@NikolajBjorner NikolajBjorner merged commit af80bd1 into Z3Prover:master Jul 14, 2022
@utaal utaal deleted the flush-trace-stream-check-sat branch July 14, 2022 21:28
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

Successfully merging this pull request may close these issues.

2 participants