1

我在 MacOS X 10.8 下使用 Z3 4.3.1（来自 master 分支）。我在以下示例中遇到分段错误：

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)


(check-sat-using qe)

任何想法，关于如何解决这个问题？

4

2 回答 2

2

我设法重现了您使用 OSX 和 Z3 4.3.1 描述的错误。此错误已修复，将在下一个正式版本中提供。同时，您可以使用 OSX 的夜间构建或使用unstable(working-in-progress) 分支构建 Z3。

可以在以下位置下载每晚构建：http: //z3.codeplex.com/releases。我们必须点击“计划中的”链接。我在这里写了一些说明。

顺便说一句，如果我们想检查可满足性，我们应该在 之后使用最终游戏策略（例如smt）qe，就像 Axel 发布的示例中一样。如果我们想检查 产生的结果qe，我们应该使用(apply qe)。

于 2013-02-19T00:49:50.613 回答
0

以下在 Windows XP + Z3 4.3.0 下工作正常

(declare-const a Int)
(declare-const b Int)

(assert
  (exists ((k Int))
    (and 
     (= (- (* 2 k) a) 0)
     (= (- (* 2 k) b) 0)
    )
  )
)
(check-sat-using (then qe smt))
(get-model)
于 2013-02-18T14:08:18.347 回答