Unfortunately, I don't know how Z3 internals work and how this
could be fixed.
Perhaps something you could try is to record the SMT queries, then feed them into Z3 directly. It should be easier to debug this way.
Maybe you could somehow reset the internal state of Z3 to a known initial state before running each query. I hope it doesn't use any non-deterministic constructs inside.
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/d5c3e76d-c4c0-41a8-b589-a8ae085401dfn%40googlegroups.com.
There is a --per-state-solver flag that allows to have a separate
solver instance in each state. See SolverManager.cpp.
Maybe setting it to true will help.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/7a22551c-05e9-42d1-92cd-dfa70a7637a5n%40googlegroups.com.