This revision was automatically updated to reflect the committed changes.
Closed by commit rC334067: [Analyzer][Z3] Test fixes for Z3 constraint manager
(authored by vlad.tsyrklevich, committed by ).
Changed prior to commit:
https://reviews.llvm.org/D47726?vs=149786&id=150076#toc
Repository:
This revision was automatically updated to reflect the committed changes.
Closed by commit rL334067: [Analyzer][Z3] Test fixes for Z3 constraint manager
(authored by vlad.tsyrklevich, committed by ).
Herald added a subscriber: llvm-commits.
Repository:
rL LLVM
https://reviews.llvm.org/D47726
george.karpenkov added a comment.
> I agree, though a number of these are limitations in CSA, and not
> specifically the backend.
Yeah, so for instance we always assume that for a given state we know whether
it's feasible or not,
and IMO for efficient SMT solver support we would need to operate
ddcc added a comment.
> @ddcc To be completely honest, I see a few design issues with the current
> implementation of Z3 backend,
> the main one being that it checks satisfiability after every single exploded
> node.
> To the best of my knowledge, reasonable scalability would not be achieved
george.karpenkov added a subscriber: mikhail.ramalho.
george.karpenkov added a comment.
@ddcc To be completely honest, I see a few design issues with the current
implementation of Z3 backend,
the main one being that it checks satisfiability after every single exploded
node.
To the best of my kn
ddcc added a subscriber: dcoughlin.
ddcc added a comment.
In https://reviews.llvm.org/D47726#1121395, @george.karpenkov wrote:
> - Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if
> that's the right thing: do all tests start to take 10x time to run once Z3 is
> enabled
george.karpenkov accepted this revision.
george.karpenkov added a comment.
This revision is now accepted and ready to land.
Seems to be good to merge regardless.
Repository:
rC Clang
https://reviews.llvm.org/D47726
___
cfe-commits mailing list
cf
george.karpenkov added a comment.
Impressive, really. So almost all tests still pass.
However, a few questions should be resolved before we can merge:
- Do all tests for Z3 run when LLVM is configured to use Z3? I'm not sure if
that's the right thing: do all tests start to take 10x time to run o
vlad.tsyrklevich created this revision.
vlad.tsyrklevich added reviewers: george.karpenkov, NoQ, ddcc.
Herald added subscribers: cfe-commits, a.sidorin, zzheng, szepet, xazax.hun.
Since Z3 tests have been not been running [1] some tests needed to be
updated. I also added a regression test for [1].
