Z3 中相同代码的不同运行时间 [英] different run time for the same code in Z3

问题描述

我用了z3的定点，发现定点的运行时间总是不一样.你遇到过同样的问题吗?为什么会这样?

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?

推荐答案

如果您从相同的状态开始获得大量的相同代码，这听起来很意外.如果您从不同的状态开始(即如果您对 Z3 进行了杂项调用无论是通过文本 API 还是编程 API，在回合之间).Z3 否则不应表现出极大的非确定性行为.非确定性行为可能由错误引起，因此如果您能进一步、更准确地描述正在执行它的场景，我们将不胜感激.

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.

这篇关于Z3 中相同代码的不同运行时间的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！