Performance Issues with Incremental Solving

[AnirudhNarsipur]

For a static analysis project, I'm using Z3 4.13.0 through the Python api. I use a combination of theories: arrays, (linear) arithmetic, strings and bitvectors (I was originally using datatypes but noticed better performance representing them as bitvectors).

I need to make repeated queries to the solver to check the current status of the constraints. However, I'm noticing performance blowups for even relatively simple instances.

This seems to be purely due to incremental solving as opposed to the difficulty of the problems. When I extract out the smtlib2 file from instances that timeout in Python (more than 60 seconds), z3 is able to solve them almost instantly (0.1 s). If I add multiple (check-sat) queries to the smtlib file the same instance now takes significantly longer (8s).

I don't use any push/pops and only use assumptions.

Is there any way I can improve performance here or at the very least get the Python API to be close in performance to directly invoking the solver with a smtlib2 file?

I've attached example smtlib2 files. These are meant purely to illustrate the performance problem and are not minimized.

Thanks!
singlequery.txt
multiquery.txt