diff options
| author | lianah <lianahady@gmail.com> | 2013-05-01 15:31:10 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-05-01 15:31:10 -0400 |
| commit | a0cf1089d3d9c36b4493de3e0498464bb50d950b (patch) | |
| tree | ea6a9db886bf905afedbfb2836625174f7d80f5e /src/theory/bv/theory_bv.cpp | |
| parent | 54e6807cec9523a3f5b5279e5a5fce8f9ba4f76a (diff) | |
removed tracing code causing slowdown; cleaned up some code
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 6f450d08e..4c31f3f44 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -173,14 +173,9 @@ void TheoryBV::check(Effort e) return; } - if (Theory::fullEffort(e)) { - Trace("bitvector-fulleffort") << "TheoryBV::fullEffort \n"; - printFacts( Trace("bitvector-fulleffort") ); - } - while (!done()) { TNode fact = get().assertion; - checkForLemma(fact); + // checkForLemma(fact); for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->assertFact(fact); } |