summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.cpp
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-01-28 19:04:25 -0500
committerlianah <lianahady@gmail.com>2013-01-28 19:04:25 -0500
commit5aec0f36fb2e896c24ce122a79bd70678371a249 (patch)
treee267ea1a4b45af5ab386c1b0fcdebe56d2cb203e /src/theory/bv/theory_bv.cpp
parentdf01ef792cf9806782b12bc93ddaa139d75346c0 (diff)
compiling implementation of new slicer finished; need to add debugging information and debug.
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r--src/theory/bv/theory_bv.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 1c746fafa..64662d5c6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -210,7 +210,6 @@ Node TheoryBV::ppRewrite(TNode t)
void TheoryBV::presolve() {
Debug("bitvector") << "TheoryBV::presolve" << endl;
- d_slicer.computeCoarsestBase();
}
bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback