[PATCH] D110357: [Analyzer] Extend ConstraintAssignor to handle remainder op

[Balázs Benics via Phabricator via cfe-commits]

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