steakhal accepted this revision.
steakhal added a comment.
I see. Now it looks correct.
Next time we shall have a z3 proof about the theory.
`A => B` <=> `not(A) or B`. which is SAT only if `A and not(B)` UNSAT.
a = z3.BitVec('a', 32)
b = z3.BitVec('b', 32)
zero = z3.BitVecVal(0, 32)
s = z3.Solver()
s.add((a % b) != zero)
s.add(a == zero)
s.check() # reports UNSAT
Note: it requires the `z3-solver` pip package.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D110357/new/
https://reviews.llvm.org/D110357
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
