0

I used fixedpoint of z3, and I found that the running time of the fixedpoint is always different. Have you meet the same problem? why does this happen?

  • 1
    Don't be too shy to provide more information. How much does the runtime vary? 1%, 10%, 100%? Can you reduce your code to a minimal example that illustrates the behaviour? – Malte Schwerhoff Jul 30 '12 at 07:12

1 Answers1

1

Sounds unexpected if you get large variety for the same code starting from the same state. If you start from different states (that is, if you have made miscellaneous calls to Z3 whether over the text API or programmatic API, between the rounds). Z3 should otherwise not exhibit hugely non-deterministic behavior. Non-deterministic behavior may arise from bugs, so it will be appreciated if you can further and more precisely describe the scenario that is exercising it.

Nikolaj Bjorner
  • 461
  • 2
  • 2