z3 - z3 和 muZ 用于计算程序不变量

Question

我正在尝试使用 z3 (muZ) 的定点求解器，以找到程序不变量。但是，在某些时候，查询回答 unsat 但我不知道为什么，因为代码是可以访问的：

(declare-rel b1 (Int) interval_relation bound_relation)
(declare-rel b2 (Int) interval_relation bound_relation)
(declare-rel b3 (Int Int) interval_relation bound_relation)
(declare-rel b4 (Int Int) interval_relation bound_relation)
(declare-rel b5 (Int Int) interval_relation bound_relation)
(declare-rel b6 (Int) interval_relation bound_relation)

(declare-var i Int)
(declare-var j Int)

(rule (b1 0))
(rule (=> (and (b1 i) (< i 50)) (b2 i)))
(rule (=> (b2 i) (b3 i 0)))
(rule (=> (and (b3 i j) (< j 50)) (b4 i j)))
(rule (=> (b4 i j) (b3 (+ i 1) (+ j 1))))
(rule (=> (and (b3 i j) (>= j 50)) (b5 i j)))
(rule (=> (b5 i j) (b1 (+ 1 (- i j)))))
(rule (=> (and (b1 i) (>= i 50)) (b6 i)))

(query (b3 i j)
  :compile-with-widening true
  :unbound-compressor false
  :engine datalog
  :print-answer true
)
 ; answers unsat

(query (b4 i j)
  :compile-with-widening true
  :unbound-compressor false
  :engine datalog
  :print-answer true
)
; answers sat
; (and (<= 0 (:var 1)) (<= (:var 1) 49))
; this invariant is correct

; corresponding C program:
; int f() {
;   int i = 0;
;   int j = 0;
; 
;   while (i < 50) {  // b1
;       j = 0;
;       while (j < 50) {  // b3
;           i++;
;           j++;
;       }
;       i = i-j+1;
;   }
;   return i;
; }

有人能解释一下为什么它返回“unsat”吗？谢谢你的帮助。

Answer 1

这是当前 Z3 版本（muZ 部分）中的一个错误。当与区间和边界域一起应用时，它会影响数据记录引擎。它现在已在本地（不稳定）分支中修复。该修复程序将在下一个版本中提供。