Open
Description
This issue starts logging all SMT queries sent to the solver during each test in bench/. Logs are written to a queries_log.jsonl file per test.
What works
- Each query is logged as JSON (hash + assumptions).
- Most tests correctly generate the log file.
- Uses QUERY_LOG_PATH to control where the child process logs.
Known issues
- Some tests don’t produce the log file (likely due to crashes or early exits).
- No timing or performance info is logged yet.
Next steps
- Ensure all tests write a log file (even if empty).
- Add query timing, memory, and CPU metrics.
- Improve error reporting if file creation fails.
How to use
git clone https://github.com/felixL-K/smtml -b trace-smt-queries
cd smtml && dune b @install && dune install
git clone https://github.com/felixL-K/owi -b trace-queries2
cd owi && dune exec -- testcomp/testcomp.exe <your-test-id>
Metadata
Metadata
Assignees
Labels
No labels