smt2lib log does not lead to a valid log

[SolalPirelli]

Separate issue originally mentioned in #5655.

I have a Python program using Z3 (via angr) without parallelism.

Here's the log from z3.set_param('solver.smtlib2_log', '/tmp/z3log'): https://transfer.sh/get/OpJJk3/z3log

It's broken in two ways: some statements start before others have ended, such as line 1364: (and (= allocated_fracs_3_v_294_8 al(check-sat, while some lines start with a bunch of NUL chars, e.g. lines 2045 and 2086.

I originally thought I might be accidentally using Z3 in a multithreaded way, but given that I only get a single file even after ca2c2bb (using z3 4.8.14), perhaps Z3 itself is doing something weird with the output? Either multi-threading or seeking to the wrong offset to write would be my guesses.

[NikolajBjorner]

Could you be reusing the log? I pushed an update that truncates previous files.
The same log written by different processes could also look weird.
However, there are no internal threads that influence this log: the log is written to by the same thread you use into the API. In other words, the code that appends to the log sits right there with the code for assert_expr, check_sat, etc.

[SolalPirelli]

OK this one might indeed be my bad, indeed angr creates new solvers, hadn't thought about that 🤦‍♂️ sorry.

Is there a way to set the path of the log per-solver instead of with a global param?

[NikolajBjorner]

Here is an example:

from z3 import *

s1 = Solver()
s2 = Solver()
s1.set("smtlib2_log","log1.smt2")
s2.set("smtlib2_log","log2.smt2")
x = Bool('x')
y = Bool('y')
s1.add(x)
s2.add(y)
s1.check()
s2.check()