diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-15 12:49:20 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-15 12:49:20 -0700 |
| commit | 3ee318ec4b2930fa1234c3f49894ba343008eca3 (patch) | |
| tree | e52a1ef6232e0c566e5b10b1e15b814d78e3759e /CMakeLists.txt | |
| parent | d16c43da9e4268a03d86fd5e7e3afbabae94ad2f (diff) | |
Fix OOB access (#3383)
In theory_engine.cpp, we were calling `theoryOf()` with
`THEORY_SAT_SOLVER` as the theory id. However, `THEORY_SAT_SOLVER` is
defined as `THEORY_LAST` and thus out-of-bounds of the `d_theoryTable`
defined in theory_engine.h (which is of size `THEORY_LAST`. This commit
adds an assertion that detects the out-of-bound access and introduces a
method to turn a theory id into a string which correctly handles
`THEORY_SAT_SOLVER`.
Diffstat (limited to 'CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions