Z3 Java 绑定：为什么在 SMT2 输入文件中设置生产证明会导致错误？

问题描述

我知道在使用 Z3 的 Java 绑定时，必须在上下文和求解器中启用证明。当输入文件不包含行(set-option :produce-proofs true)时，以下程序完美运行：

   // Setup Context
    HashMap<String,String> cfg = new HashMap<String,String>();
    cfg.put("proof","true");
    Context ctx = new Context(cfg);
    
   // Read input file
    BoolExpr[] program = ctx.parseSMTLIB2File(file_name,null,null);
    
   // Create Solver
    Solver s =  ctx.mkSolver();
    s.add(program);

   // Set Solver parameters
    Params p = ctx.mkParams();
    p.add("mbqi",true);
    p.add("proof",true);
    s.setParameters(p);

   // Use Solver
    Status status = s.check();
    if(status.equals(Status.UNSATISFIABLE)) {
        Expr<?> obj = s.getProof();
    }

但是，一旦输入文件确实包含行 (set-option :produce-proofs true)，我就会在执行 parseSMTLIB2File 时收到以下错误消息：

错误设置':produce-proofs'，选项值不能修改初始化”

如果我给定的输入都包含行 (set-option :produce-proofs true)，那么在 parseSMTLIB2File 期间是否有某种方法可以忽略此行？还是我真的必须相应地修改输入文件？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

java java smt z3