string - 解决这个字符串问题时Z3可能不一致？

Question

我刚刚在弦理论中遇到了一个 SMTLIB 问题，Z3 的回答可能不一致。调用Z3 解决问题时：带参数smt.string_solver=z3str3返回unsat；没有任何参数它返回sat。

我也使用 CVC4 来解决这个问题。它返回了一个解决方案，这似乎是一个有效的模型，因为我通过手动将变量分配替换为问题来检查它。

由于我正在尝试使用 Z3 进行研究，因此我想知道这是否是 Z3 的已知行为。感谢任何可以提供帮助的人！:)

编辑：我在 WSL Ubuntu 16.04 上使用 Z3 4.7.1。

Answer 1

I'd say that getting unsat or sat, depending on Z3's configuration, sounds like a bug to me. Check the Z3 issue tracker for issues that describe a similar behaviour, and if nothing pops up, file an issue there. Ideally with a minimal example to reproduce the problem with, your current one is rather long.