Z3慢速QF_AUFBV模式

Question

我一直在檢查SMT-COMP 2015 benchmark results QF_AUFBV模式，它們令人震驚。 Same thing for 2014.

據他們說，Z3比其他SMT解算器慢幾個數量級。

我的理解是Z3和CVC4一樣快。我錯過了什麼嗎？

Regards

Answer 1

是的，這是正確的，Z3在這個類別中不是特別好。我們正在研究多種不同的技術，這些技術會對此產生影響，但他們還沒有準備好，他們並沒有直接針對這37個基準。鑑於競爭對手的基準數量很少，我們應該非常謹慎地從這些結果中得出任何結論。