summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2010-09-24 15:03:28 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2010-09-24 15:03:28 +0000
commit353c6d5c3770365f0dffcbdf697199bed156cf50 (patch)
treee8a019cf24b3a4dd2b4eb458cbe066164b6eddee /src/theory/theory_engine.h
parentbb0fc300c810f68f1e901413272c6658e31d60f9 (diff)
basic union find for bitvectors
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index cc0e663fa..074d40d05 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -332,7 +332,7 @@ public:
d_uf->check(effort);
d_arith->check(effort);
d_arrays->check(effort);
- //d_bv->check(effort);
+ d_bv->check(effort);
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback