问题描述
我想弄清楚为什么 z3 求解器为特定公式返回未知数。
该公式代表某段代码，带有执行“抽象”乘法的循环（受长乘法算法启发）。
为了检查我的抽象算法是否正确工作（通过了我的验证条件），我对条件的否定进行了编码以从 z3 中获得反例。在 z3 中编码公式可以理解地涉及展开循环。我将超时设置为 0（即无超时），并使用 SolverFor("QF_BV")。我在 parallel.enable 中使用了 40 个线程。
虽然对于宽度为 2 到 14 的位向量确实得到 unsat，但当我选择宽度为 16 的位向量时，z3 会在大约 11 小时内给我一个 unkNown（这个时间会有所不同）。
在求解器上调用 .reason_unkNown()，我得到：incomplete
(:eliminated-vars 1034
:lh-add-binary 140371855
:lh-bca 23814396
:lh-bool-var 2231207637
:lh-cube-backtracks 105014
:lh-cube-conflicts 35005
:lh-cube-cutoffs 70009
:lh-double-lookahead-propagations 2528053
:lh-double-lookahead-rounds 1241284
:lh-propagations 158526025
:lh-windfalls 26038702
:max-memory 44090.71
:memory 177.62
:num-allocs 27798866265032752.00
:par-progress 100.00
:par-unsat 34999
:rlimit-count 764946247
:sat-ate 222268
:sat-backjumps 3002301117
:sat-backtracks 147
:sat-bce 104728
:sat-conflicts 3002336240
:sat-decisions 3454552584
:sat-del-clause 3371028754
:sat-elim-bool-vars-res 1361521
:sat-elim-clauses 1059679366
:sat-elim-literals 1080799650
:sat-gc-clause 1918637627
:sat-minimized-lits 858977833
:sat-mk-clause-2ary 40013037
:sat-mk-clause-3ary 97306887
:sat-mk-clause-nary 3779658115
:sat-mk-var 556299461
:sat-probing-assigned 122001
:sat-propagations-2ary 3293681175
:sat-propagations-3ary 2950499967
:sat-propagations-nary 3439887739
:sat-restarts 371680015
:sat-scc-elim-binary 3427928
:sat-scc-elim-vars 1188920
:sat-subs-resolution 196847601
:sat-subs-resolution-dyn 1928526157
:sat-subsumed 252105065
:sat-tr 1131060
:sat-units 47282317
:time 42930.13)
这应该是什么意思，我应该如何解释？ z3 是否因为求解器认为求解时间太长而返回未知？还是因为z3连解决都解决不了，可能是理论不够表达？还是其他什么原因？
如果您需要任何细节（关于代码或 z3 编码），请告诉我。我也有一个非常详细的运行，如果需要，可以链接到一个 pastebin。
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）