summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bv_inverter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-rw-r--r--src/theory/quantifiers/bv_inverter.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 014e46925..292ec2ec6 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -202,7 +202,7 @@ static Node dropChild(Node n, unsigned index)
if (nchildren < 2) return Node::null();
Kind k = n.getKind();
- NodeBuilder<> nb(k);
+ NodeBuilder nb(k);
for (unsigned i = 0; i < nchildren; ++i)
{
if (i == index) continue;
@@ -350,7 +350,7 @@ Node BvInverter::solveBvLit(Node sv,
unsigned upper, lower;
upper = bv::utils::getSize(t) - 1;
lower = 0;
- NodeBuilder<> nb(BITVECTOR_CONCAT);
+ NodeBuilder nb(BITVECTOR_CONCAT);
for (unsigned i = 0; i < nchildren; i++)
{
if (i < index)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback