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 /src/theory/theory_engine.h | |
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 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 587d3693c..e88d3323a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -797,6 +797,7 @@ public: * @returns the theory */ inline theory::Theory* theoryOf(theory::TheoryId theoryId) const { + Assert(theoryId < theory::THEORY_LAST); return d_theoryTable[theoryId]; } |