diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 40bc2417b..91150f663 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -357,6 +357,9 @@ void TheoryBV::checkForLemma(TNode fact) { void TheoryBV::check(Effort e) { + if (done() && !fullEffort(e)) { + return; + } Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); |