z3解算器：使用“ parseSMTLIB2String”与“ rise4fun在线工具”获得不同的结果

Question

[我正在使用z3开发Java程序，但是当我使用“ parseSMTLIB2String”方法与在线工具rise4fun测试非常简单的编码时，得到了不同的结果。

下面是我的测试编码：

(declare-const s Bool)(assert (exists ((p Bool))(or (not s) p)))(check-sat)(get-model)

当我使用rise4fun在线工具对其进行测试时，它会给我结果：

sat(model(define-fun s () Boolfalse))

但是当我尝试在Java中使用“ parseSMTLIB2String”方法时，它给了我以下结果：

sat(define-fun s () Booltrue)

所以我想知道为什么他们给我不同的结果。我是否以错误的方式使用“ parseSMTLIB2String”方法？

下面是我在Java中的小型测试类：

HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
@SuppressWarnings("resource")
Context ctx = new Context(cfg);

BoolExpr[] formula = ctx.parseSMTLIB2String("(declare-fun s () Bool)\n" + 
  "(assert (exists ((p Bool))(or (not s) p)))", null, null, null, null);

Solver s = ctx.mkSolver();
s.add(formula);

Status result = s.check();

if (result == Status.SATISFIABLE){  
  System.out.println("sat");
  Model m = s.getModel();
  System.out.println(m.toString());
}  

Answer 1

rise4fun没有运行Z3的最新版本；现在很有可能已经很老了。对于约束(exists ((p Bool))(or (not s) p))，true和false都是s的正确解。

（（仅供参考：parseSMTLIB2String仅解析输入文件中的断言，这与在SMT2文件上运行命令行Z3并不完全相同。）