diff options
| author | Tim King <taking@cs.nyu.edu> | 2018-08-21 12:58:05 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-21 12:58:05 -0700 |
| commit | 1f469ae989f692502d1dc845d51f5319be10311c (patch) | |
| tree | a1d1f932e8c05e31da79045cdd7888745c13cc76 /src/theory/bv | |
| parent | 290f2a718a8ebe9532239fa53fabc9763564b5dc (diff) | |
Add constexpr annotations to help coverity understand constant ... (#2314)
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 541b77fe6..1b7eeddac 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -861,9 +861,11 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) } // Propagate differs depending on the subtheory - // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain + // * bitblaster needs to be left alone until it's done, otherwise it doesn't + // know how to explain // * equality engine can propagate eagerly - bool ok = true; + // TODO(2348): Determine if ok should be set by propagate. If not, remove ok. + constexpr bool ok = true; if (subtheory == SUB_CORE) { d_out->propagate(literal); if (!ok) { |