diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
index 02392a6f33..c7087a887c 100644
--- a/lib/Solver/BitwuzlaBuilder.cpp
+++ b/lib/Solver/BitwuzlaBuilder.cpp
@@ -537,13 +537,6 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> e, int *width_out) {
     Term left = construct(ce->getLeft(), width_out);
     Term right = construct(ce->getRight(), width_out);
     Term eq = eqExpr(left, right);
-    unsigned numKids = ce->getNumKids();
-    std::vector<Term> term_args;
-    term_args.reserve(numKids);
-
-    for (unsigned i = 0; i < numKids; ++i) {
-      term_args.push_back(construct(ce->getKid(i), 0));
-    }
 
     *width_out = ce->getWidth();
     return iteExpr(eq, left, null);
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index b957212771..4ca6b69eaa 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -748,6 +748,19 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
     break;
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+
+    *width_out = ce->getWidth();
+    res = evaluate(
+        _solver,
+        metaSMT::logic::Ite(
+            construct(EqExpr::create(ce->getLeft(), ce->getRight()), 0),
+            construct(ce->getLeft(), width_out),
+            construct(ConstantExpr::create(0, ce->getWidth()), width_out)));
+    break;
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     assert(ce);
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 0a40aca824..7c0e537f14 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -627,6 +627,17 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return res;
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    ExprHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    ExprHandle left = construct(ce->getLeft(), width_out);
+    ExprHandle right = construct(ce->getRight(), width_out);
+    ExprHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return vc_iteExpr(vc, eq, left, null);
+  }
+
   case Expr::Extract: {
     ExtractExpr *ee = cast<ExtractExpr>(e);
     ExprHandle src = construct(ee->expr, width_out);
diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp
index a61b26388c..7b61e1b67b 100644
--- a/lib/Solver/Z3BitvectorBuilder.cpp
+++ b/lib/Solver/Z3BitvectorBuilder.cpp
@@ -7,6 +7,7 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
+#include "Z3Builder.h"
 #include "klee/Config/config.h"
 
 #ifdef ENABLE_Z3
@@ -339,6 +340,17 @@ Z3ASTHandle Z3BitvectorBuilder::constructActual(ref<Expr> e, int *width_out) {
     return iteExpr(cond, tExpr, fExpr);
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    Z3ASTHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    Z3ASTHandle left = construct(ce->getLeft(), width_out);
+    Z3ASTHandle right = construct(ce->getRight(), width_out);
+    Z3ASTHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return iteExpr(eq, left, null);
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     unsigned numKids = ce->getNumKids();
diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp
index 8d1930e311..6761dd4b62 100644
--- a/lib/Solver/Z3CoreBuilder.cpp
+++ b/lib/Solver/Z3CoreBuilder.cpp
@@ -266,6 +266,17 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> e, int *width_out) {
     return iteExpr(cond, tExpr, fExpr);
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    Z3ASTHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    Z3ASTHandle left = construct(ce->getLeft(), width_out);
+    Z3ASTHandle right = construct(ce->getRight(), width_out);
+    Z3ASTHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return iteExpr(eq, left, null);
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     unsigned numKids = ce->getNumKids();