QF_NIA腳本立即用Z3 4.3.2終止，但不是用4.4.2

Question

這個script幾乎沒有時間用Z3 4.3.2產生一個正確的模型，但似乎永遠用Z3 4.4.2運行並在幾秒鐘後超時在Rise4fun上。 n=5（鏈接的鏈接有n=4）的腳本版本也在4.3.2上運行很長時間。我試圖改變sat.random_seed和smt.random_seed，但無濟於事。我還能嘗試什麼？

Answer 1

謝謝你的例子。現在比特衝擊波檢測到這是有限域。它沒有處理「獨特」，因此回到使用超昂貴的Groebner基計算的默認解算器。它可以關閉，但更好地修復有限域檢測。