Inconsistent results in CLI and Z3Py API

[izycheva]

Hi,

I am using Z3 to check loop invariants, and noticed that Python API sometimes returns UNKNOWN for the same queries where the command line interface returns SAT.

Here is the relevant code snippet of how I compare the outputs:

s = z3.Solver()
# ... # building the query across multiple files    
result = s.check()
if result == Result.SAT:
   # ... # process the model
elif result == Result.UNKNOWN:
   timestamp = time.time_ns()
   f = open(f'query_ind{timestamp}.sl', 'w')
   q = s.to_smt()
   f.write(q)
   f.close()
   res = subprocess.run(["z3", f"query_ind{timestamp}.sl", "-model"], capture_output=True)
   formatted_result = res.stdout.decode('utf-8').strip('\n').upper()
   print(f"CLI result {formatted_result}, and is it equal to the API {result.name}? {result.name == res}") 
   raise Exception(f'Error or timeout init query, see "query_ind{timestamp}.sl"')

which prints

CLI result SAT, and is it equal to the API UNKNOWN? False

I also tried importing the file as shown below and then the solver returns SAT (as CLI).

out = z3.parse_smt2_file("query_ind1750080013035511000.sl")
s.add(out)
s.check() # returns SAT

My code relies on the API output, and I did not use to have this issue in the older version of Z3Py (though, last I used it was 2020).
This seems like a potential bug in calling the solver internally in the Python API or the printing of the query into a string. Could you please check which one it is?
For now the workaround of printing to a file and reading from it works for me, but if the printing is wrong, I'd need a different fix.
Thanks in advance!

I am using Z3 version 4.15.1 - 64 bit, Python bindings installed with pip, Python version 3.12.4. Also attaching the file for which the API returned UNKOWN (txt added to be able to upload on GitHub):
query_ind1750080013035511000.sl.txt