错误的结果从z3

我试图用Z3 SMT求解器证明以下内容：((x*x) + x) = ((~x * ~x) + ~x)。这是正确的，因为c语言中的溢出语义。错误的结果从z3

现在，我写了下面的SMT-LIB代码：

(declare-fun a() Int) 

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296)) 
(define-fun mynot ((x Int))   Int (- 4294967295 (mod x 4294967296))) 
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296)) 

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x)))) 
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x))) 

(simplify (myfun1 0)) 
(simplify (myfun2 0)) 

(assert (= (myfun1 a) (myfun2 a))) 
(check-sat) 
(exit)

输出从Z3是：

0 
0 
unsat

现在我的问题：为什么结果是 “不饱和度”？我的代码中的简化命令显示可以获得有效的分配，以便myfun1和myfun2具有相同的结果。

我的代码有问题，或者这是z3中的错误？

请任何人都可以帮助我。 Thx

来源

2012-01-25 Thomas

如果你打算使用C类整数，除非这是手动编码练习，我建议你使用位向量而不是数学整数。 – Philippe

快速评论：这个不正确的结果是由于Z3公式预处理器中的错误。它已经修复，修复程序将在下一个版本中提供。该错误会影响使用以下格式的公式的基准：'（mod（+ a b））'或'（mod（* a b））'。 –

@GManNickG：好点，我会做的。 –

错误的结果是由于Z3公式/表达式预处理器中的错误造成的。该bug已经修复，并且已经是当前版本的一部分（v4.3.1）。受影响的基准测试使用以下格式的公式：(mod (+ a b))或(mod (* a b))。

我们可以在线重试示例here，并获得预期结果。

来源

2013-02-02 13:36:37

错误的结果从z3

回答

相关问题