z3 SMT解算器：運行後的未知結果QF_BVRE基準測試

Question

我剛剛下載了seq和regexp排序的基準測試（使用z3-4.3.2）。運行「membership_1.smt2」後，如果結果未知，可能會出現什麼問題？

我沒有指定任何進一步的命令行選項。根據基準，它應該導致坐下，但未知的打印沒有任何模型。

謝謝

編輯：

我注意到進一步，即 「重新開始」 不被認可。這與z3的版本有關，還是你忘了命令行選項？

Answer 1

首先，我不知道OP或評論者在哪裏找到了「membership_1.smt2」示例輸入。我檢查了SMT-LIB benchmarks，以及Z3，S3和Z3-str的源代碼，但無法找到它。

無論如何，問題在於OP正在測試爲S3或Z3-str編寫的基準測試，並針對Z3的未修改版本運行測試。 S3和Z3-str需要修改版本的Z3來處理這些擴展。這是在S3網站上描述S3：針對Web安全的分析，http://www.comp.nus.edu.sg/~trinhmt/S3/，訪問2016年8月4日一個符號串求解]：

修改Z3的版本求解

• 的源代碼修改後的Z3可用here。
• 我們修改Z3使弦理論和算術理論之間有相互作用。

• 這些新增的API方法允許我們查詢字符串變量的長度以及字符串變量的不同長度之間的關係，如our CCS'14 paper所示。

• 對於integer/string theory integration，我們對Z3的修改版本也使用Z3-str GROUP。

Grepping的(unmodified) Z3 source沒有顯示出了 「重新開始」 或 「重新CONCAT」 的比賽。對修改後的版本進行修改顯示，這些修改在的z3-source-060115.zip中定義。