[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

Fri Jun 4 15:23:54 PDT 2021

manas added a comment.

In D103440#2799629 <https://reviews.llvm.org/D103440#2799629>, @xazax.hun wrote:

> I was wondering, if we could try something new with the tests. To increase our confidence that the expected behavior is correct, how about including a Z3 proof with each of the test cases?

We are looking forward to design a unit-test framework for the solver which can compact the test cases and make them much more manageable (unlike `constant-folding.c`). Perhaps, we can incorporate the Z3 proves in that framework, corresponding to test cases.

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103440/new/

https://reviews.llvm.org/D103440